Somesh Jha , University of Wisconsin
Semantic Adversarial Deep Learning
Fueled by massive amounts of data, models produced by machine-learning (ML) algorithms, especially deep neural networks, are being used in diverse domains where trustworthiness is a concern, including automotive systems, finance, health care, natural language processing, and malware detection. Of particular concern is the use of ML algorithms in cyber-physical systems (CPS), such as self-driving cars and aviation, where an adversary can cause serious consequences.
However, existing approaches to generating adversarial examples and devising robust ML algorithms mostly ignore the semantics and context of the overall system containing the ML component. For example, in an autonomous vehicle using deep learning for perception, not every adversarial example for the neural network might lead to a harmful consequence. Moreover, one may want to prioritize the search for adversarial examples towards those that significantly modify the desired semantics of the overall system. Along the same lines, existing algorithms for constructing robust ML algorithms ignore the specification of the overall system. In this paper, we argue that the semantics and specification of the overall system has a crucial role to play in this line of research. We present preliminary research results that support this claim.
Eran Yahav, Technion
From Programs to Interpretable Deep Models, and Back
Shaz Qadeer, Microsoft Research, and Bernhard Kragl, IST
Proving a concurrent program correct by demonstrating it does nothing
CIVL is a verifier for concurrent programs implemented as a conservative extension to the Boogie verification system. CIVL allows the proof of correctness of a concurrent program —shared-memory or message-passing— to be described as a sequence of program layers. The safety of a layer implies the safety of the layer just below, thus allowing the safety of the highest layer to transitively imply the safety of the lowest.
The central theme in CIVL is reasoning about atomic actions. Different layers of a program describe its behavior using atomic actions, higher layers with coarse-grained and lower layers with fine-grained atomic actions. A proof of correctness amounts to a demonstration that the highest layer is SKIP, the atomic action that does nothing. The formal and automated verification justifying the connection between adjacent layers combines several techniques—linear variables, reduction based on movers, location invariants, and procedure-local abstraction.
CIVL is available in the master branch of Boogie together with more than fifty micro-benchmarks. CIVL has also been used to reﬁne a realistic concurrent garbage-collection algorithm from a simple high-level speciﬁcation down to a highly-concurrent implementation described in terms of individual memory accesses.
Matteo Maffei, TU Wien, and Clara Schneidewind, TU Wien
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics.
This tutorial will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently introduced, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode that comes with a proof of soundness.