-
Scalable Polyhedral Verification of Recurrent Neural Networks
Authors:
Wonryong Ryou,
Jiayu Chen,
Mislav Balunovic,
Gagandeep Singh,
Andrei Dan,
Martin Vechev
Abstract:
We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and nonlinear recurrent update functions by combining sampling, optimization, and Fermat's theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem tha…
▽ More
We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and nonlinear recurrent update functions by combining sampling, optimization, and Fermat's theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.
△ Less
Submitted 10 June, 2021; v1 submitted 27 May, 2020;
originally announced May 2020.
-
Synthesizing Unrestricted False Positive Adversarial Objects Using Generative Models
Authors:
Martin Kotuliak,
Sandro E. Schoenborn,
Andrei Dan
Abstract:
Adversarial examples are data points misclassified by neural networks. Originally, adversarial examples were limited to adding small perturbations to a given image. Recent work introduced the generalized concept of unrestricted adversarial examples, without limits on the added perturbations. In this paper, we introduce a new category of attacks that create unrestricted adversarial examples for obj…
▽ More
Adversarial examples are data points misclassified by neural networks. Originally, adversarial examples were limited to adding small perturbations to a given image. Recent work introduced the generalized concept of unrestricted adversarial examples, without limits on the added perturbations. In this paper, we introduce a new category of attacks that create unrestricted adversarial examples for object detection. Our key idea is to generate adversarial objects that are unrelated to the classes identified by the target object detector. Different from previous attacks, we use off-the-shelf Generative Adversarial Networks (GAN), without requiring any further training or modification. Our method consists of searching over the latent normal space of the GAN for adversarial objects that are wrongly identified by the target object detector. We evaluate this method on the commonly used Faster R-CNN ResNet-101, Inception v2 and SSD Mobilenet v1 object detectors using logo generative iWGAN-LC and SNGAN trained on CIFAR-10. The empirical results show that the generated adversarial objects are indistinguishable from non-adversarial objects generated by the GANs, transferable between the object detectors and robust in the physical world. This is the first work to study unrestricted false positive adversarial examples for object detection.
△ Less
Submitted 19 May, 2020;
originally announced May 2020.
-
Cryptocurrency with Fully Asynchronous Communication based on Banks and Democracy
Authors:
Asa Dan
Abstract:
Cryptocurrencies came to the world in the recent decade and attempted to offer a new order where the financial system is not governed by a centralized entity, and where you have complete control over your account without the need to trust strangers (governments and banks above all). However, cryptocurrency systems face many challenges that prevent them from being used as an everyday coin. In this…
▽ More
Cryptocurrencies came to the world in the recent decade and attempted to offer a new order where the financial system is not governed by a centralized entity, and where you have complete control over your account without the need to trust strangers (governments and banks above all). However, cryptocurrency systems face many challenges that prevent them from being used as an everyday coin. In this paper we attempt to take one step forward by introducing a cryptocurrency system that has many important properties. Perhaps the most revolutionary property is its deterministic operation over a fully asynchronous communication network, which has sometimes been mistakenly considered to be impossible. By avoiding any temporal assumptions, we get a system that is robust against arbitrary delays in the network, and whose latency is only a function of the actual communication delay. The presented system is based on familiar concepts $-$ banking and democracy. Our banks, just like normal banks, keep their clients' money and perform their clients' requests. However, because of the cryptographic scheme, your bank cannot do anything in your account without your permission and its entire operation is transparent so you don't have to trust it blindly. The democracy means that every operation performed by the banks (e.g., committing a client transaction) has to be accepted by a majority of the coin holders, in a way that resembles representative democracy where the banks are the representatives and where each client implicitly delegates his voting power (the sum of money in his account) to his bank. A client can switch banks at any moment, by simply applying a corresponding request to the new bank of his choice.
△ Less
Submitted 25 September, 2019; v1 submitted 13 April, 2019;
originally announced April 2019.
-
Securify: Practical Security Analysis of Smart Contracts
Authors:
Petar Tsankov,
Andrei Dan,
Dana Drachsler Cohen,
Arthur Gervais,
Florian Buenzli,
Martin Vechev
Abstract:
Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts.
To address this problem, we present Securify, a security analyzer for Ethereum smart contr…
▽ More
Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts.
To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language.
Securify is publicly released, it has analyzed >18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.
△ Less
Submitted 24 August, 2018; v1 submitted 4 June, 2018;
originally announced June 2018.
-
On Using Time Without Clocks via Zigzag Causality
Authors:
Asa Dan,
Rajit Manohar,
Yoram Moses
Abstract:
Even in the absence of clocks, time bounds on the duration of actions enable the use of time for distributed coordination. This paper initiates an investigation of coordination in such a setting. A new communication structure called a zigzag pattern is introduced, and shown to guarantee bounds on the relative timing of events in this clockless model. Indeed, zigzag patterns are shown to be necessa…
▽ More
Even in the absence of clocks, time bounds on the duration of actions enable the use of time for distributed coordination. This paper initiates an investigation of coordination in such a setting. A new communication structure called a zigzag pattern is introduced, and shown to guarantee bounds on the relative timing of events in this clockless model. Indeed, zigzag patterns are shown to be necessary and sufficient for establishing that events occur in a manner that satisfies prescribed bounds. We capture when a process can know that an appropriate zigzag pattern exists, and use this to provide necessary and sufficient conditions for timed coordination of events using a full-information protocol in the clockless model.
△ Less
Submitted 24 May, 2017;
originally announced May 2017.
