Tools and Algorithms for the Construction and Analysis of Systems

Inhaltsverzeichnis

1. Frontmatter

   PDF-Version jetzt herunterladen

2. Synthesis

   1. Frontmatter

   2. HOLL: Program Synthesis for Higher Order Logic Locking

      • Open Access

      Gourav Takhar, Ramesh Karri, Christian Pilato, Subhajit Roy

      Abstract

      Logic locking “hides” the functionality of a digital circuit to protect it from counterfeiting, piracy, and malicious design modifications. The original design is transformed into a “locked” design such that the circuit reveals its correct functionality only when it is “unlocked” with a secret sequence of bits—the key bit-string. However, strong attacks, especially the SAT attack that uses a SAT solver to recover the key bit-string, have been profoundly effective at breaking the locked circuit and recovering the circuit functionality.

      We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-order relation, instead of a key of independent values, challenging the attacker to discover this key relation to recreate the circuit functionality. Our technique uses program synthesis to construct the locked design and synthesize a corresponding key relation. HOLL has low overhead and existing attacks for logic locking do not apply as the entity to be recovered is no more a value. To evaluate our proposal, we propose a new attack (SynthAttack) that uses an inductive synthesis algorithm guided by an operational circuit as an input-output oracle to recover the hidden functionality. SynthAttack is inspired by the SAT attack, and similar to the SAT attack, it is verifiably correct, i.e., if the correct functionality is revealed, a verification check guarantees the same. Our empirical analysis shows that SynthAttack can break HOLL for small circuits and small key relations, but it is ineffective for real-life designs.

      PDF-Version jetzt herunterladen

   3. The Complexity of LTL Rational Synthesis

      • Open Access

      Orna Kupferman, Noam Shenwald

      Abstract

      In rational synthesis, we automatically construct a reactive system that satisfies its specification in all rational environments, namely environments that have objectives and act to fulfill them. We complete the study of the complexity of LTL rational synthesis. Our contribution is threefold. First, we tighten the known upper bounds for settings that were left open in earlier work. Second, our complexity analysis is parametric, and we describe tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components. Third, we generalize the definition of rational synthesis, combining the cooperative and non-cooperative approaches studied in earlier work, and extend our complexity analysis to the general definition.

      PDF-Version jetzt herunterladen

   4. Synthesis of Compact Strategies for Coordination Programs

      • Open Access

      Kedar S. Namjoshi, Nisarg Patel

      Abstract

      In multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordination can be difficult. In this work, we develop theory and methods to synthesize coordination strategies that are guaranteed not to initiate unnecessary actions. We refer to such strategies as being “compact.” We formalize the intuitive notion of compactness; show that existing methods do not guarantee compactness; and propose a solution. The solution transforms a given temporal logic specification, using automata-theoretic constructions, to incorporate a notion of minimality. The central result is that the winning strategies for the transformed specification are precisely the compact strategies for the original. One can therefore apply known synthesis methods to produce compact strategies. We report on prototype implementations that synthesize compact strategies for temporal logic specifications and for specifications of multi-robot coordination.

      PDF-Version jetzt herunterladen

   5. ZDD Boolean Synthesis

      • Open Access

      Yi Lin, Lucas M. Tabajara, Moshe Y. Vardi

      Abstract

      Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.

      PDF-Version jetzt herunterladen

3. Verification

   1. Frontmatter

   2. Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems

      • Open Access

      André Greiner-Petter, Howard S. Cohl, Abdou Youssef, Moritz Schubotz, Avi Trost, Rajen Dey, Akiko Aizawa, Bela Gipp

      Abstract

      Digital mathematical libraries assemble the knowledge of years of mathematical research. Numerous disciplines (e.g., physics, engineering, pure and applied mathematics) rely heavily on compendia gathered findings. Likewise, modern research applications rely more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both digital mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a novel approach to verify a digital mathematical library and two computer algebra systems with one another by converting mathematical expressions from one system to the other. We use our previously developed conversion tool (referred to as ) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems Maple and Mathematica. The contributions of our presented work are as follows: (1) we present the most comprehensive verification of computer algebra systems and digital mathematical libraries with one another; (2) we significantly enhance the performance of the underlying translator in terms of coverage and accuracy; and (3) we provide open access to translations for Maple and Mathematica of the formulae in the NIST Digital Library of Mathematical Functions.

      PDF-Version jetzt herunterladen

   3. Verifying Fortran Programs with CIVL

      • Open Access

      Wenhao Wu, Jan Hückelheim, Paul D. Hovland, Stephen F. Siegel

      Abstract

      Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran’s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application.

      PDF-Version jetzt herunterladen

   4. NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems

      • Open Access

      Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, Marco Zamboni

      Abstract

      We present Norma, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). Norma is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed nuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. Norma is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations.

      PDF-Version jetzt herunterladen

   5. Efficient Neural Network Analysis with Sum-of-Infeasibilities

      • Open Access

      Haoze Wu, Aleksandar Zeljić, Guy Katz, Clark Barrett

      Abstract

      Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, DeepSoI, to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI. Extending the complete search with DeepSoI achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.

      PDF-Version jetzt herunterladen

4. Blockchain

   1. Frontmatter

   2. Formal Verification of the Ethereum 2.0 Beacon Chain

      • Open Access

      Franck Cassez, Joanne Fuller, Aditya Asgaonkar

      Abstract

      We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain’s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at https://github.com/ConsenSys/eth2.0-dafny.

      PDF-Version jetzt herunterladen

   3. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

      • Open Access

      David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Emma Zhong

      Abstract

      The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.

      PDF-Version jetzt herunterladen

   4. A Max-SMT Superoptimizer for EVM handling Memory and Storage

      • Open Access

      Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio

      Abstract

      Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present \(\textsf {GASOL}^{v2}\), a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. \(\textsf {GASOL}^{v2}\) can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler solc, and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by solc.

      PDF-Version jetzt herunterladen

5. Grammatical Inference

   1. Frontmatter

   2. A New Approach for Active Automata Learning Based on Apartness

      • Open Access

      Frits Vaandrager, Bharat Garhewal, Jurriaan Rot, Thorsten Wißmann

      Abstract

      We present \(L^{\#}\), a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the \(L^{*}\) algorithm and its descendants, \(L^{\#}\) takes a different perspective: it tries to establish apartness, a constructive form of inequality. \(L^{\#}\) does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. \(L^{\#}\) has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of \(L^{\#}\) in practice. Experiments with a prototype implementation, written in Rust, suggest that \(L^{\#}\) is competitive with existing algorithms.

      PDF-Version jetzt herunterladen

   3. Learning Realtime One-Counter Automata

      • Open Access

      Véronique Bruyère, Guillermo A. Pérez, Gaëtan Staquet

      Abstract

      We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin’s \({L}^*\) algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.

      PDF-Version jetzt herunterladen

   4. Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

      • Open Access

      Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider

      Abstract

      Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning formulas in fragments of LTL without the \(\mathbf {U}\)-operator for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.

      PDF-Version jetzt herunterladen

   5. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

      • Open Access

      Luca Bortolussi, Giuseppe Maria Gallo, Jan Křetínský, Laura Nenzi

      Abstract

      We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.

      PDF-Version jetzt herunterladen