ABSTRACT. In this talk, we will share our experience in the successful deployment of verified software in a wide range of application domains, and, importantly, our insights on the key factors enabling such successful deployment, in particular the importance of the social aspects of a group working effectively together.

Our formally verified microkernel, seL4, is now used across the world in a number of applications that keeps growing. Our experience is that such an uptake is enabled not only by a technical strategy, but also by a tight integration of people from multiple disciplines and with both research and engineering profiles. This requires a strong social culture, with well designed processes, for working as one unified team. We share our observations on what concrete social structures have been key for us in creating real-world impact from research breakthroughs.

ABSTRACT. Dataflow graphs are typically used to model signal processing applications. Consistency is a necessary condition for the existence of a dataflow graph schedule using bounded memory. Existing methods to check this property are based on a static analysis. At every modification on the dataflow graph, the consistency property has to be checked again and on the entire graph, after its construction. In this paper, we argue that for each modification, the consistency can be checked only on the modified graph elements, and during its construction. We propose an alternative method, that can be applied either on the entire graph, or locally, at each modification of a dataflow graph. For both cases, we analyse our algorithm's advantages, and compare its performance to an existing algorithm. For the experimental setup, we generate random graphs with worst-case instances and realistic instances. Our theoretical analysis shows that the proposed algorithm can reduce the number of operations required for the consistency verification, even on entire graphs. The experimental results show that our algorithm outperforms the state-of-the-art algorithm on the considered benchmark.

ABSTRACT. Kalman filters are widely used for estimating the state of a system based on noisy or inaccurate sensor readings, for example in the control and navigation of vehicles or robots. However, numerical instability may lead to divergence of the filter, and establishing robustness against such issues can be challenging. We propose novel formal verification techniques and software to perform a rigorous quantitative analysis of the effectiveness of Kalman filters. We present a general framework for modelling Kalman filter implementations operating on linear discrete-time stochastic systems, and techniques to systematically construct a Markov model of the filter's operation using truncation and discretisation of the stochastic noise model. Numerical stability properties are then verified using probabilistic model checking. We evaluate the scalability and accuracy of our approach on two distinct probabilistic kinematic models and several implementations of Kalman filters.

ABSTRACT. Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of complex heap objects like trees and lists. Testing such programs is challenging due to multiple reasons. Firstly, test inputs for such program are required to satisfy non-trivial constraints which must be specified precisely. Secondly, precisely encoding and solving path conditions in such programs are challenging and often expensive. In this work, we propose the first concolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort.

ABSTRACT. Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as Hyper-LTL, support a rich set of such properties. We first show that black-box monitoring of HyperLTL is in general unfeasible, and suggest a gray-box approach. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorabiliy (the feasibility of solving the monitoring problem). Thus, as another contribution of this paper we refine the classic notions of monitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty called distributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.

ABSTRACT. This paper proposes a method to systematically extract the formal semantics of ARM instructions from their natural language specifications. Although ARM is based on RISC architecture and the number of instructions is rather small, a large number of variations diversely exist under various series such as Cortex-A, Cortex-M, and Cortex-R. Thus, the automatic extraction of the formal semantics of rather simple instructions reduces human efforts for tools development, such as symbolic execution engines. We focus on 6 variations, M0, M0+, M3, M4, M7, and M33 of ARM Cortex-M, aiming to analyze IoT malware. Our natural language processing consists of the semantics interpretation by applying translation rules, augmented by the similarity analysis among sentences for distinguishing the modification of flags. Among 1039 specifications of instructions collected from the internet, the formal semantics of 662 instructions have been successfully extracted. They are utilized afterward to preliminarily build a dynamic symbolic execution engine for ARM Cortex-M called Corana, which is able to directly analyze binary files. We experimentally observe that Corana effectively traces IoT malware under the presence of obfuscation techniques like indirect jumps.

ABSTRACT. This paper introduces GOSPEL, a behavioral specification language for OCaml. It is designed to enable modular verification of data structures and algorithms. GOSPEL is a contract-based, strongly typed language, with a formal semantics defined by means of translation into Separation Logic. Compared with writing specifications directly in Separation Logic, GOSPEL provides a high-level syntax that greatly improves conciseness and makes it accessible to programmers with no familiarity with Separation Logic. Although GOSPEL has been developed for specifying OCaml code, we believe that many aspects of its design could apply to other programming languages. This paper presents the design and semantics of GOSPEL, and reports on its application for the development of a formally verified library of general-purpose OCaml data structures.

ABSTRACT. Matching Logic is a framework for specifying programming language semantics and reasoning about programs. Its formulas are called patterns and are built with variables, symbols, connectives and quantifiers. A pattern is a combination of structural components (term patterns), which must be matched, and constraints (predicate patterns), which must be satisfied. Dealing with more than one structural component in a pattern could be cumbersome because it involves multiple matching operations. A source for getting patterns with many structural components is the conjunction of patterns. Here, we propose a method that uses a syntactic unification algorithm to transform conjunctions of structural patterns into equivalent patterns having only one structural component and some additional constraints. We prove the soundness and the completeness of our approach, and we provide sound strategies to generate certificates for the equivalences.

ABSTRACT. The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code.

In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present the enabling technology ProB 2.0, a Java API to the ProB animator and model checker. We describe several case studies that use ProB 2.0 to interact with a formal specification at runtime.

ABSTRACT. Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not it is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. In this paper, we illustrate how instruction reordering allowed by contemporary multicore processors leads to vulnerabilities in such programs, and present a compositional, timing-sensitive information-flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread's security by tracking information about dependencies between instructions which guarantee their order of occurrence. Program security can then be established from individual thread security using rely/guarantee reasoning.

ABSTRACT. This paper explores formal verification in the area of database technology, in particular how to reason about queries and updates in a database system. The formalism is sufficiently general to be applicable to relational and graph databases. We first define a domain-specific language consisting of nested query and update primitives, and give its operational semantics. Queries are in full first-order logic. The problem we try to solve is whether a database satisfying a given pre-condition will satisfy a given post-condition after execution of a given sequence of queries and updates. We propose a weakest-precondition calculus and prove its correctness. We finally examine a restriction of our framework that produces formulas in the guarded fragment of predicate logic and thus leads to a decidable proof problem.

ABSTRACT. Separation logic handles \emph{data abstraction} adequately, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of \emph{subsumption}. We demonstrate \emph{function-specification subtyping}, analogous to subtyping, with a \emph{subsumption} rule: if $\sigma$ is a \lstinline{funspec_sub} of $\tau$, that is $\sigma \subtype \tau$, then $x:\sigma$ implies $x:\tau$, meaning that any function satisfying specification $\sigma$ can be used wherever a function satisfying $\tau$ is demanded. We extend previous notions of Hoare-logic sub-specification, which already included parameter adaption, to include \emph{framing} (necessary for separation logic) and impredicative bifunctors (necessary for higher-order functions, i.e. function pointers). We show how this enables compositional modular verification of the functional correctness of C programs, in Coq, with foundational machine-checked proofs of soundness.

ABSTRACT. Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.

ABSTRACT. This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been implemented, so Ethereum contracts can now also be executed on IELE. The VM automatically generated from the semantics of IELE is shown to have adequate performance. Indeed, a major blockchain (hidden for now, to keep the anonymity of the authors) has deployed the thus generated VM. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM.

ABSTRACT. To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.

ABSTRACT. Automated reasoning about systems with infinite domains requires an extension of automata to infinite alphabets. One such model is Variable Finite Automata (VFA). VFAs are finite automata whose alphabet is interpreted as variables that range over an infinite domain. On top of their simple and intuitive structure, VFAs have many appealing properties. One such property is a deterministic fragment (DVFA), which is closed under the Boolean operations, and whose containment and emptiness problems are decidable. These properties are unique amongst the many different models for automata over infinite alphabets. In this paper, we continue to explore the advantages of DVFAs, and show that they have a canonical form, which proves them to be a particularly robust model that is easy to reason about and work with. Building on these results, we construct an efficient learning algorithm for DVFAs, based on the L^* algorithm for regular languages.

ABSTRACT. Automata learning techniques automatically generate system models from test observations. These techniques usually fall into two categories: passive and active. Passive learning uses a predetermined data set, e.g., system logs. In contrast, active learning actively queries the system under learning, which is considered more efficient.

An influential active learning technique is Angluin's L* algorithm for regular languages which inspired several generalisations from DFAs to other automata-based modelling formalisms. In this work, we study L*-based learning of Markov decision processes, first assuming an ideal setting with perfect information. Then, we relax this assumption and present a novel learning algorithm that collects information by sampling system traces via testing. Experiments with the implementation of our sampling-based algorithm suggest that it achieves better accuracy than state-of-the-art passive learning techniques with the same amount of test observations. In contrast to existing learning algorithms with predefined states, our algorithm learns the complete model structure including the states.

ABSTRACT. This paper proposes novel reachability algorithms for both exact (sound and complete) and over-approximation (sound) analysis for deep neural networks (DNNs). The approach uses star sets as a symbolic representation of sets of states, which are known in short as stars and provide an effective representation of high-dimensional polytopes. Our star-based reachability algorithms can be applied to several problems in analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. Our star-based reachability algorithms are implemented in a software prototype called the neural network verification (NNV) tool that is publicly available for evaluation and comparison. Our experiments show that when verifying ACAS Xu neural networks on a multi-core platform, our exact reachability algorithm is on average about 19 times faster than Reluplex, a satisfiability modulo theory (SMT)-based approach. Furthermore, our approach can visualize the precise behavior of DNNs because the reachable states are computed in the method. Notably, in the case that a DNN violates a safety property, the exact reachability algorithm can construct a complete set of counterexamples. Our star-based over-approximate reachability algorithm is on average 100 times faster than Reluplex on the verification of properties for ACAS Xu networks, even without exploiting the parallelism that comes naturally in our method. Additionally, our over-approximate reachability is much less conservative than DeepZ and DeepPoly, recent approaches utilizing zonotopes and other abstract domains that fail to verify many properties of ACAS Xu networks due to their conservativeness. Moreover, our star-based over-approximate reachability algorithm obtains better robustness bounds in comparison with DeepZ and DeepPoly when verifying the robustness of image classification DNNs.

ABSTRACT. A general, compositional, and component-based contract theory is proposed for modeling and specifying heterogeneous systems, characterized by consisting of parts from different domains, e.g. software, electrical and mechanical. Given a contract consisting of assumptions and a guarantee, clearly separated conditions on a component and its environment are presented where the conditions ensure that the guarantee is fulfilled—a responsibility assigned to the component, given that the environment fulfills the assumptions. The conditions are applicable whenever it cannot be ensured that the sets of ports of components are partitioned into inputs and outputs, and hence fully support scenarios where components, characterized by both causal and acausal models, are to be integrated by solely relying on the information of a contract. An example of such a scenario of industrial relevance is explicitly considered, namely a scenario in a supply chain where the development of a component is outsourced. To facilitate the application of the theory in practice, necessary properties of contracts are also derived to serve as sanity checks of the conditions. Furthermore, based on a graph that represents a structuring of a hierarchy of contracts, sufficient conditions to achieve compositionality are presented.

ABSTRACT. Service-oriented architecture (SOA) is a popular architectural style centered around services, loose coupling, and interoperability. A recurring problem in SOA development is the Button Problem; how to ensure that whenever a "button is pressed" on some service—no matter what—the performance of other key services remains unaffected? The Button Problem is especially complex to solve in systems that over time have devolved into hardly comprehensible spaghettis of service dependencies. In a collaborative effort with industry partner First8, we present the first formal framework to help SOA developers solve the Button Problem, enabling automated reasoning about service sensitivities and candidate refactorings. Our formalization provides a rigorous foundation for a tool that was successfully applied in industrial case studies, and it is built against two unique requirements: “whiteboard level of abstraction” and non-quantitative analysis.

ABSTRACT. A salient objective of studying gene regulatory networks (GRNs) is to identify potential target genes whose perturbations would lead to effective treatment of diseases. In this paper, we develop two control methods for GRNs in the context of asynchronous Boolean networks. Our methods compute a minimal subset of nodes of a given Boolean network, such that temporary or permanent perturbations of these nodes drive the network from an initial state to a target steady state. The main advantages of our methods include: (1) temporary and permanent perturbations can be feasibly conducted with techniques for genetic modifications in biological experiments; and (2) the minimality of the identified control sets can reduce the cost of experiments to a great extent. We apply our methods to several real-life biological networks in silico to show their efficiency in terms of computation time and their efficacy with respect to the number of nodes to be perturbed.