Search

Dynamic Binary Translation (DBT) is a powerful approach to support cross-architecture emulation of unmodified binaries. However, DBT systems face correctness and performance challenges, when emulating concurrent binaries from strong to weak memory consistency architectures. As a matter of fact, we report several translation errors in QEMU, when emulating x86 binaries on Arm hosts. To address these challenges, we propose an end-to-end approach that provides correct and efficient emulation for weak memory model architectures. Our contributions are twofold: First, we formalize QEMU’s intermediate representation’s memory model, and use it to propose formally verified mapping schemes to bridge the strong-on-weak memory consistency mismatch. Second, we implement these verified mappings in Risotto, a QEMU-based DBT system that optimizes memory fence placement while ensuring correctness. Risotto further improves performance via cross-architecture dynamic linking of native shared libraries and faster yet correct translation of compare-and-swap operations. We evaluate Risotto using multi-threaded benchmark suites and real-world applications, and show that Risotto improves the emulation performance by 6.7% on average over “erroneous” QEMU, while ensuring correctness. Postprint

Application development for the modern Web involves sophisticated engineering workflows which include user interface aspects. Those involve Web elements typically created with HTML/CSS markup and JavaScript-like languages, yielding Web documents. WebMonitor leverages requirements formally specified in a logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. Then, requirements are verified upon arbitrary web pages, allowing for automated support for a wide set of use cases in interaction testing and simulation. We position WebMonitor within a developer workflow, where in case of a negative result, a visual counterexample is returned. The monitoring framework we present follows a black-box approach, and as such is independent of the underlying technologies a Web application may be developed with, as well as the browser and operating system used. WebMonitoris available as open source software: https://github.com/ennioVisco/webmonitor Video demonstration of WebMonitor: https://youtu.be/hqVw0JU3k9c

The World Wide Web Consortium (W3C) introduced the Thing Description (TD), a standardized and unified human- and machine-readable semantic description of Internet of Things (IoT) devices that focuses on describing how to interact with the described device using its network-interfaces. However, the TDs lack a way to describe the physical effect of said interactions on the device itself, as well as on the environment around the device, limiting its viability for cyber-physical scenarios. In this paper, we propose an extension for describing the effects of an interaction on the property affordances of a Thing in the TD as a first step towards a TD that is able to fully describe a Cyber-Physical System (CPS). We show this extension permits the generation of accurate Digital Twins, facilitates machine-aided system design and device mashup generation and allows for formal verification of the functionality of CPSs during their deployment and maintenance.

MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

International audience; EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify postquantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

Concurrent systems software is widely-used, complex, and error-prone, posing a significant security risk. We introduce VRM, a new framework that makes it possible for the first time to verify concurrent systems software, such as operating systems and hypervisors, on Arm relaxed memory hardware. VRM defines a set of synchronization and memory access conditions such that a program that satisfies these conditions can be mostly verified on a sequentially consistent hardware model and the proofs will automatically hold on relaxed memory hardware. VRM can be used to verify concurrent kernel code that is not data race free, including code responsible for managing shared page tables in the presence of relaxed MMU hardware. Using VRM, we verify the security guarantees of a retrofitted implementation of the Linux KVM hypervisor on Arm. For multiple versions of KVM, we prove KVM's security properties on a sequentially consistent model, then prove that KVM satisfies VRM's required program conditions such that its security proofs hold on Arm relaxed memory hardware. Our experimental results show that the retrofit and VRM conditions do not adversely affect the scalability of verified KVM, as it performs similar to unmodified KVM when concurrently running many multiprocessor virtual machines with real application workloads on Arm multiprocessor server hardware. Our work is the first machine-checked proof for concurrent systems software on Arm relaxed memory hardware.

This paper reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By "lightweight formal methods"we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods experts to check new features and properties as ShardStore has evolved., SOSP '21: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, ISBN:978-1-4503-8709-5

The operation of trimming data sets is heavily used in AI systems. Trimming is useful to make AI systems more robust against adversarial or common perturbations. At the core of robust AI systems lies the concept that outliers in a data set occur with low probability, and therefore can be discarded with little loss of precision in the result. The statistical argument that formalizes this concept of robustness is based on an extension of the Chebyshev’s inequality first proposed by Tukey in 1960. In this paper we present a mechanized proof of robustness of the trimmed mean algorithm, which is a statistical method underlying many complex applications of deep learning. For this purpose we use the Coq proof assistant to formalize Tukey’s extension to Chebyshev’s inequality, which allows us to verify the robustness of the trimmed mean algorithm. Our contribution shows the viability of mechanized robustness arguments for algorithms that are at the foundation of complex AI systems.

International audience; Rewriting is a widely established formalism with major applications in computer science. It is indeed a staple of many formal verification applications as it is especially well suited to describe program semantics and transformations. In particular, constructor based term rewriting systems are generally used to illustrate the behaviour of functional programs.In the context of formal verification, it is often necessary to characterize the shape of the reducts of such rewrite systems and, in a typed context, the underlying type system provides syntactic guarantees on the form of these terms by exhibiting, among others, the constructor symbols that they can contain. On the other hand, when performing (program) transformations we often want to eliminate some symbols and, more generally, to ensure that some patterns are absent from the result of the transformation.We propose in this paper an approach to statically verify the absence of specified patterns from the reachable terms of constructor based term rewriting systems. The proposed approach consists in annotating the function symbols with a set of profiles outlining pre- and post-conditions that must be verified by the rewrite relation, and using a rewrite based method to statically verify that the rewrite system is indeed consistent with the respective annotations.

A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.

Highly-configurable software underpins much of our computing infrastructure. It enables extensive reuse, but opens the door to broken configuration specifications. The configuration specification language, Kconfig, is designed to prevent invalid configurations of the Linux kernel from being built. However, the astronomical size of the configuration space for Linux makes finding specification bugs difficult by hand or with random testing. In this paper, we introduce a software model checking framework for building Kconfig static analysis tools. We develop a formal semantics of the Kconfig language and implement the semantics in a symbolic evaluator called kclause that models Kconfig behavior as logical formulas. We then design and implement a bug finder, called kismet, that takes kclause models and leverages automated theorem proving to find unmet dependency bugs. kismet is evaluated for its precision, performance, and impact on kernel development for a recent version of Linux, which has over 140,000 lines of Kconfig across 28 architecture-specific specifications. Our evaluation finds 781 bugs (151 when considering sharing among Kconfig specifications) with 100% precision, spending between 37 and 90 minutes for each Kconfig specification, although it misses some bugs due to underapproximation. Compared to random testing, kismet finds substantially more true positive bugs in a fraction of the time.

In Vehicular Ad hoc NETworks (VANETs), vehicles exchange safety messages containing valuable information about traffic environment to increase roads’ safety. The critical nature of these messages entails securing them before considering them. In this context, the credibility and the accuracy assessment of these included safety information arises as a necessity since the consumption of false or imprecise ones by vehicles may cause hazardous consequences. To treat this requirement, we proposed the scheme [1] enabling vehicles to evaluate the credibility and the accuracy of the contents of the safety messages exchanged in VANETs. That scheme is based on three modules: a reputation module, a time and location closeness estimation module, and a majority module. A vehicle can use these modules in a separated or joint way according to the circumstances. Since that scheme is error prone, we conducted in [2], a formal validation, using inference system, to prove the soundness and the completeness of these three modules and their combination. In this paper, we complete that formal validation of [1] by handling the junctions of the three basic modules two by two. To do this, we first completed the inference system in [2] so that the junctions of the three modules two by two become incorporated. A formal verification using this holistic inference system was proposed in a second step to prove the soundness and the completeness of these junctions. This verification's obtained results confirmed the validity of the said junctions for being sound and complete.

The security of protocols and the absence of design-related weaknesses and vulnerabilities is crucial for the prevention of cyber attacks. This paper provides the first formal model for EnOcean, an IoT protocol widely used in home automation systems. Based on EnOcean’s security specification a formal model of its teach-in and high security authentication is created in the applied pi calculus. In an automated security analysis with the security protocol model checker ProVerif several security requirements are checked. While the analysis shows that all the secrecy statements can be verified, it identifies some weaknesses for the authentication. Based on an analysis of the potential attacks, we suggest a provable fix for the detected attacks.

The diversity of paths on the Internet makes it difficult for designers and operators to confidently deploy new congestion control algorithms (CCAs) without extensive real-world experiments, but such capabilities are not available to most of the networking community. And even when they are available, understanding why a CCA underperforms by trawling through massive amounts of statistical data from network connections is challenging. The history of congestion control is replete with many examples of surprising and unanticipated behaviors unseen in simulation but observed on real-world paths. In this paper, we propose initial steps toward modeling and improving our confidence in a CCA's behavior. We have developed CCAC, a tool that uses formal verification to establish certain properties of CCAs. It is able to prove hypotheses about CCAs or generate counterexamples for invalid hypotheses. With CCAC, a designer can not only gain greater confidence prior to deployment to avoid unpleasant surprises, but can also use the counterexamples to iteratively improvetheir algorithm. We have modeled additive-increase/multiplicative-decrease (AIMD), Copa, and BBR with CCAC, and describe some surprising results from the exercise.

The application of deep reinforcement learning (DRL) to computer and networked systems has recently gained significant popularity. However, the obscurity of decisions by DRL policies renders it hard to ascertain that learning-augmented systems are safe to deploy, posing a significant obstacle to their real-world adoption. We observe that specific characteristics of recent applications of DRL to systems contexts give rise to an exciting opportunity: applying formal verification to establish that a given system provably satisfies designer/user-specified requirements, or to expose concrete counter-examples. We present whiRL, a platform for verifying DRL policies for systems, which combines recent advances in the verification of deep neural networks with scalable model checking techniques. To exemplify its usefulness, we employ whiRL to verify natural equirements from recently introduced learning-augmented systems for three real-world environments: Internet congestion control, adaptive video streaming, and job scheduling in compute clusters. Our evaluation shows that whiRL is capable of guaranteeing that natural requirements from these systems are satisfied, and of exposing specific scenarios in which other basic requirements are not.

Videogame level designs can contain errors called softlocks where a player traversing the level in an unintended manner can become permanently stuck. In this paper, we explore the automated detection of softlocks in the game Super Metroid using Computation Tree Logic (CTL). Super Metroid distinguishes itself as an example domain because of its velocity-based movement and rich item upgrade hierarchy. These factors can cause softlocks in Super Metroid to be challenging to detect visually. We contribute a tile-based gameplay abstraction for Super Metroid, and demonstrate verification of CTL properties for scenarios based on a segment of the original game’s level design. CTL can be used to define and test many other gameplay properties (e.g. which bosses can be skipped or which order items may be collected) and is immediately applicable to other game designs for which a compact abstraction of their state space can be enumerated. By making plausible design changes to a Super Metroid level fragment, we show how highly nonobvious softlocks can be detected and how the counterexamples resulting from verification failure can be turned into visualizations that explain the problem.

Considering the importance of workflow model in the modern business process, we propose an alternative way to modify the ordinary YAWL workflow which is one of the popular and simple models, to be able to validate and verify the workflow time performance. By introducing a time duration of a task in the YAWL workflow as the time constraints, it would be relevantly transformed into a corresponding timed automata which is suitable to be simulated and verified against the fundamental properties, such as safetyness and liveness properties. A set of transforming rules are proposed to map a given YAWL workflow with time constraints into the resulting timed automata. The tasks and their decorators indicating the splitting and joining of the workflow, would be considered, and transformed into synchronizing channels in timed automata. The time duration of a task would be handled using the relevant local clock in the timed automata. Finally, the resulting timed automata is correctly simulated and verified using the UPPAAL simulation tool.

Single flux quantum (SFQ) circuits as an example of superconducting electronics (SCE) have the potential to replace CMOS circuits as they possess a theoretical potential of three orders of magnitude reduction in power accompanied with one order of magnitude higher speed. Despite its benefits, the SCE community lacks a reliable open source formal verification solution. This paper proposes a verification framework called qMC, a model checker for SFQ circuits using formal techniques. qMC offers an automated process that constructs a SystemVerilog testbench consisting of formal assertions to verify the SFQ-specific properties of the circuits and produce system correctness results and counterexamples using model checking (MC). Instead of creating an MC tool from scratch, we have built qMC based on well established open source back-end verification engines for MC of CMOS circuits, including Yosys-SMTBMC and EBMC. qMC allows for properties to be given in SystemVerilog formal assertions, time-limited SystemVerilog assertions, or linear temporal logic (LTL). qMC provides an improvement in terms of verification time and coverage when compared to state-of-the-art semi-formal based SFQ verification frameworks. For instance, verification time for a 4-bit array multiplier is sped up by 19.5x.

To enable trust in the IC supply chain, logic locking as an IP protection technique received significant attention in recent years. Over the years, by utilizing Boolean satisfiability (SAT) solver and its derivations, many de-obfuscation attacks have undermined the security of logic locking. Nonetheless, all these attacks receive the inputs (locked circuits) in a very simplified format (Bench or remapped and translated Verilog) with many limitations. This raises the bar for the usage of the existing attacks for modeling and assessing new logic locking techniques, forcing the designers to undergo many troublesome translations and simplifications. This paper introduces the RANE Attack, an open-source CAD-based toolbox for evaluating the security of logic locking mechanisms that implement a unique interface to use formal verification tools without a need for any translation or simplification. The RANE attack not only performs better compared to the existing de-obfuscation attacks, but it can also receive the library-dependent logic-locked circuits with no limitation in written, elaborated, or synthesized standard HDL, such as Verilog. We evaluated the capability/performance of RANE on FOUR case studies, one is the first de-obfuscation attack model on FSM locking solutions (e.g., HARPOON) in which the key is not a static bit-vector but a sequence of input patterns.

Verifying processors has been and still is a major challenge. Therefore, intensive research has led to advanced verification solutions ranging from ISS-based reference models, (cross-level) simulation down to formal verification at the RTL. During the verification of the processor implementation at the Instruction Set Architecture (ISA) level, test stimuli, i.e. test programs are needed. They are either created manually or with the aid of sophisticated test program generators. However, significant effort is required to produce thorough test programs. In this paper, we devise a novel approach for processor verification by Equivalent Program EXecution (EPEX). Our approach is based on a new form of equivalence checking Instead of comparing the architectural states of two models which execute the same program P, we derive a second, but equivalent program P^ from P (wrt. to a formal ISA model), and check that executing P and P^ will produce equal architectural states on the same design. We show that EPEX can easily be used in a simulation-based verification environment and broadens existing tests automatically. In a RISC-V case study using different core configurations of the well-known VexRiscv core, we demonstrate the bug-finding capabilities of EPEX.

The interfaces between layers of a system are susceptible to bugs if developers of adjacent layers proceed under subtly different assumptions. Formal verification of two layers against the same formal model of the interface between them can be used to shake out these bugs. Doing so for every interface in the system can, in principle, yield unparalleled assurance of the correctness and security of the system as a whole. However, there have been remarkably few efforts that carry out this exercise, and all of them have simplified the task by restricting interactivity of the application, inventing new simplified instruction sets, and using unrealistic input and output mechanisms. We report on the first verification of a realistic embedded system, with its application software, device drivers, compiler, and RISC-V processor represented inside the Coq proof assistant as one mathematical object, with a machine-checked proof of functional correctness. A key challenge is structuring the proof modularly, so that further refinement of the components or expansion of the system can proceed without revisiting the rest of the system.

Ethereum is a platform for deploying smart contracts, which due to their public nature and the financial value of the assets they manage are attractive targets for attacks. With asset management as a main task of smart contracts, access control aspects are naturally part of the application itself, but also of the functions implemented in a smart contract. Therefore, it is desirable to establish the correctness of smart contracts and their access control on application and single-function level through formal methods. However, there is no established methodology of formalising and verifying correctness properties of smart contracts. In this work, we make an attempt in this direction on the basis of a case study. We choose an existing smart contract application which aims to ascertain the integrity of binary files distributed over the Internet by means of decentralised identity management and access control. We formally specify and verify correctness at the level of single functions as well as temporal properties of the overall application. We demonstrate how to use verified low-level correctness properties for showing correctness at the higher level. In addition, we report on our experience with existing verification tools.

The new 5G technology has the ability to create logical communication networks, called network slices, which are specifically carved to serve particular application domains. Due to the mix of applications criticality, it becomes crucial to verify if the applications’ service level agreements are met, especially for the mission-critical scenarios, before the system is up and running. In this paper, we propose a novel framework for modeling and verifying 5G orchestration of dynamic services, which considers simultaneous access of network slices, admission of new requests to slices, virtual network function scheduling, and routing. Due to the dynamic nature of the problem such verification becomes a challenging issue. By combining the benefits of modeling in user-friendly UML, with model checking using UPPAAL, our framework helps to address the issue by enabling both modeling and formal verification at design stage. We demonstrate our approach on a case study that involves: (i) a mission-critical 5G-assisted robot surgery e-health application, accomplished by using a health slice that is simultaneously accessed by various health professionals using a 5G-enabled camera, and (ii) a less critical video streaming application using a video slice, accessed via various 5G-enabled mobile phones, within the same area as the robotic application. By employing our approach, one can verify that the critical health application meets its timeliness requirements, but also that all slices are eventually served in the system.

Many online transaction scheduler architectures and algorithms for various software transactional memories have been designed in order to maintain good system performance even for high concurrency workloads. Most of these algorithms were directly implemented in a target programming language, and experimentally evaluated, without theoretical proofs of correctness and analysis of their performance. Only a small number of these algorithms were modeled using formal methods, such as process algebra CSP, in order to verify that they satisfy properties such as deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods has its disadvantages, too. In this paper, we first analyze the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this analysis, we correct and extend the CSP model. Finally, based on PAT results for the new CSP model, we analyze the performance of PSTM online transaction scheduling algorithms from the perspective of makespan, number of aborts, and throughput. Based on our findings, we may conclude that for the complete formal verification of trustworthy software, both formal verification and it's testing must be jointly used., Comment: 18 pages, 5 figures, 5 tables, 4 algorithms

We propose an automatic verification method for cryptographic protocols. Our method can verify whether or not the key-exchange protocol satisfies main security properties, requiring only the protocol specification as its input. The specification consists of, for example, how session keys are computed and which party sends/receives which data to/from the communication channel. We materialize our method using the Tamarin prover, which is an automatic verification tool for cryptographic protocols. To show the validity of our method, we verify main security properties of several existing protocols and find that the results coincide with what are theoretically known in cryptography. Our method is effective, because the complexity of cryptographic protocols has significantly increased in recent years. To overcome the complexity, people have started using automatic verification tools to verify the security of cryptographic protocols, but existing tools have two problems. First, the user must be familiar with the details of cryptography in order to describe formally the security model as part of input. Second, the input code is complex and its creation is error-prone; protocol specification and security model must be written in a specific language together with protocol-dependent extra codes. These two problems are resolved by our method.

This work studies formal verification of continuous-time continuous-space systems with unknown dynamics against safety specifications. The proposed framework is based on a data-driven construction of barrier certificates using which the safety of unknown systems is verified via a finite set of data collected from trajectories of systems with a priori guaranteed confidence. In the proposed scheme, we first cast the original safety problem as a robust convex program (RCP). Since the unknown model appears in one of the constraints of the proposed RCP, we provide the scenario convex program (SCP) corresponding to the original RCP by collecting finite numbers of data from systems' evolutions. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP. Accordingly, we formally quantify the safety guarantee of unknown systems based on the number of data and the required level of safety confidence. Motivations. In the past few years, formal methods have become a promising approach to analyze dynamical systems against high-level logic properties, e.g., those expressed as linear temporal logic (LTL) formulae, in a reliable way. In this regard, barrier certificates, as a discretization-free approach, have received significant attention as a useful tool for formal analysis of complex dynamical systems. In particular, barrier certificates are Lyapunov-like functions defined over the state space of systems subjected to a set of inequalities on both the function itself and its time derivative along the flow of the system. The existence of such a function provides a formal certificate for the safety of the system [1, 2]. To employ the proposed approaches in the setting of barrier certificates, one needs to know precise models of dynamical systems and, hence, those approaches are not applicable where the model is unknown. Although there are some identification techniques in the relevant literature to first learn the model and then provide the analysis framework (e.g., [3, 4]), acquiring an accurate model for complex systems is always very challenging, time-consuming, and expensive. This crucial challenge motivated us to employ data-driven approaches and directly construct barrier certificates via data collected from trajectories of unknown systems.

Modern cyber-physical systems (CPS) interact with the physical world, hence their correctness is important. In this work, we build upon the Simplex Architecture, where control authority may switch from an unverified and potentially unsafe advanced controller to a verified-safe baseline controller in order to maintain system safety. We take the approach further by lifting the requirement that the baseline controller must be verified or even correct, instead also treating it as a black-box component. This change is important; there are many types of powerful control techniques---model predictive control and neural network controllers---that often work well in practice, but are unlikely to be formally proven correct due to complexity. We prove such an architecture maintains safety, and present case studies where model-predictive control provides safety for multi-robot coordination, and unverified neural networks provably prevent collisions for groups of F-16 aircraft.

In recent years, there has been a great deal of interest and research in verifying complex cyber-physical systems (CPS) against rich and expressive specifications [2] such as safety and liveness, to provide formal guarantees for safety-critical systems. While linear temporal logic (LTL) [1] can capture these properties of interest, it is incapable of specifying many information-flow properties that rely on information of multiple traces. These properties, which are described over sets of traces, are called hyperproperties [4] and their corresponding temporal logics have been well studied. The extension of LTL to capture a fragment of hyperproperties, namely, HyperLTL [3], makes use of trace variables to specify individual execution traces and allows for quantification of trace variables to precede a (trace) quantifier-free formula. Here, we present a sound approach for verifying discrete-time control systems against HyperLTL formulae through the use of so-called augmented barrier certificates (ABCs).

Autonomous driving systems may encounter situations where it is necessary to transfer control to the human driver, for instance when encountering unpredictable dangerous road conditions. To be able to do so safely, the autonomous system needs an estimate of how long it will take for the human driver to take control of the vehicle. A neural network can be used for making such predictions. However ensuring that such a neural network can be used in safety-critical situations is very challenging. We discuss our recent efforts for building, analysing and formally verifying a neural network built for predicting takeover time in a shared-control autonomous driving system. The network was trained on data collected from a (semi-) autonomous driving simulator. We evaluated several techniques for the analysis of the neural network as follows. We performed robustness and sensitivity analysis for the neural network, using the Marabou formal verification tool. We evaluated off-the-shelf attribution tools to determine the important features upon which the neural network makes its predictions. We investigated trust and confidence analysis to better understand the neural network outputs. And finally, we performed adversarial training to improve the quality of the neural network. We discuss our results and outline directions for future work.

The exploitation of smart-contract vulnerabilities can lead to catastrophic losses. Formal verification can be a useful tool in identifying these vulnerabilities before deployment. We present an encoding of Solidity and the Ethereum blockchain using Boogie, an intermediate verification language. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. Distinctive features of our encoding are precisely capturing Solidity's unorthodox memory model, a notion of lazy blockchain exploration, and memory-precise verification harnesses. Unlike much of the work in this area, our modus operandi is not matching contracts against specific known behavioural patterns that might lead to vulnerabilities. Rather, we provide a tool to find errors/bad states - be they vulnerabilities or not - that might be reached through behaviours that might not follow such a pattern.

We present a formal verification method that provides a model-based approach to human-robot interaction (HRI) in medical settings by utilizing linear temporal logic (LTL). We define high-level HRI procedures with an LTL-based framework to create algorithmically sound robots that can function independently in dynamic HRI environments. Our approach's theoretical infallibility confers particular advantages for medical robots, where safety and informative communications are crucial. In order to establish the viability of our proposed method, and with the ongoing COVID-19 pandemic in mind, we developed an LTL knowledge base for a medical robot tasked with HRI-intensive roles of patient reception and triage. We designed robotic simulations based on our LTL architecture to test our approach, employing randomized inputs to generate unpredictable HRI environments. We then conducted formal verification via an automata-theoretic approach by evaluating our simulated robot against generalized Buchi automata. We hope our LTL-based approach can enable future achievements in HRI.

The goal of this research is to contribute a new component to challenge existing automated verification tools. This component is a generic copy capability extension to an existing map concept. It is designed with proper formal specifications and loop invariants so that it is amenable to verification. The map concept and the extension both avoid explicit references and aliasing. The copy capability is implemented using a loop that goes through the entire map, pulling out each value in the map to copy, and then placing that value back into the original map and its copy, thereby keeping the original map the same while creating the copy. Verification of the extension using the RESOLVE verifying compiler successfully generates verification conditions, though they are not proved automatically at this time. The copy extension can serve as an instructive example to teach Computer Science students about formal verification of iterative code with loop invariants.

Testing-based formal verification with symbolic execution (TBFV-SE) checks whether programs correctly implement their formal specification. Given a formal specification and a program, it first derives a theorem expressing the correctness property of the executed program paths and then formally verifies the validity of the theorem. However, such theorems still need to be verified manually due to the lack of a tool support for dealing with expressions involved. In this paper, we propose a method for automatically verifying theorems for TBFV-SE. This method uses an SMT solver to check whether a theorem is valid. For this purpose, the method converts the conditions in the theorems written in the SOFL specification language into appropriate constraints that are supported by the SMT solver. We present a tool to support the method, and present two case studies to demonstrate how the tool works in the context of Java programs and SOFL specifications.

The hardware security of space VLSI is an important issue of the reliable operation of spacecraft system in orbit. This paper focuses on the security evaluation method of VLSI design front-end based on formal verification theory. This method is adopted in the security check of a space Application Specific Integrated Circuit (ASIC). Using assertions of key registers, the potential design vulnerability of ASIC is found, which can lead to tampering of configuration data tampering under lock-in mode, and resulting in abnormal reset and even downtime of the whole chip. Finally, the security design improvement suggestions are given against the tampering.

Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs can help to enable efficient dynamic participation (e.g., in consensus) and reduce storage overhead. In this paper, we formalize an AAOSL originally described by Maniatis and Baker, and prove its key correctness proper- ties. Our model and proofs are machine checked in Agda. Our proofs apply to a generalization of the original construction and provide confidence that instances of this generalization can be used in practice. Our formalization effort has also yielded some simplifications and optimizations.

This presentation will describe how we are using, and aiming to use, runtime verification, along with other varieties of formal verification and simulation-based testing, to together provide increased confidence in a range of autonomous systems.

Cryptographic algorithms are widely used to protect data privacy in many aspects of daily lives from smart card to cyber-physical systems. Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis of the correlation between power consumptions of an electronic device and private data. To thwart these attacks, several masking schemes have been proposed. However, programs that rely on secure masking schemes are not secure a priori. Although some techniques have been proposed for formally verifying masking countermeasures and for quantifying masking strength, they are currently limited to Boolean programs and suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is more accurate for arithmetic programs and more scalable for Boolean programs comparing to the existing approaches. We have implemented our methods in a verification tool QMVerif which has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning.

Implantable Medical Devices (IMDs) have evolved over the years to stretch their application areas to provide a range of services from health-care to public safety. In order to handle such information, the high strength security and the proper authentication are required. For this, Ellouze et al. have proposed an authentication protocol for IMDs in 2013. The security in IMD that they propose and mention is reasonable, but some aspects are expected to be vulnerable to attack. In addition, not only are such schemes need to be secured, but their security should also be formally verified against their security requirements. Thus, we confirm the security of the authentication protocol for IMDs that have not been objectively verified through formal verification tool such as BAN-logic. Consequently, in this paper, Ellouze et al. are turned out to be insecure.

Implantable Medical Devices (IMDs) play a very critical role in both medical and non-medical fields. Hence, protecting the security and privacy of these devices is among the highest priorities, as failing to do so would jeopardize the life of the patient. One way of maintaining the safety of IMDs is to design an authentication protocol between the IMDs and the external devices. With this regard, although several authentication schemes exist, a significant number of these protocols did not include formal verification to prove their secrecy against known attacks. One such authentication scheme is the He and Zeadally protocol for IMD-Enabled Ambient Assisted Living System. Accordingly, in this paper, we analyzed the security of this protocol by using formal verification methods -BAN-Logic and AVISPA. As a result, despite the protocol's strong qualities, we found that the protocol is insecure and fell short of other essential such as emergency authentication and key-update procedures.

While formal verification techniques are inevitable to ensure safety of critical cyber-phyical systems (CPS), engineering techniques to support the design and analysis of such CPS are still in their infancy. Therefore, we take a first step towards the provision of appropriate engineering techniques for CPS verification, by providing an extensive evaluation of the current state of the art, identifying challenges not yet tackled by existing approaches and by proposing a research roadmap intended to pave the way towards a fully supported engineering process for CPS verification models.

Advances in silicon integration technology have allowed the emergence of extremely complex Systems-on-Chip and Application-Specific Integrated Circuits. This complexity impacted severely the verification time and effort of delayed products, that due to this they often miss the market window. Engineering teams have experienced exponential verification time increase with the linear complexity increase and the largest proportion of effort is due to segmented, long, tedious, bug-prone and repetitive low level verification. This work presents a High-level Synthesis – driven formal verification method, aimed in quickly verifying high-level software or hardware code which rapidly converges results from different abstraction levels in a formal design flow. First the benefits of formal techniques are explained and the proposed methodology is outlined. Then 4 converging aspects of our formal methodology, and namely high-level program code verification, cycle-accurate verification, RTL verification and automatically-generated test-benches are explained, discussed and cross-compared. The aim is to rapidly converge all types of possible formal verification types before the final implementation is ported to the manufacturer to create the IC. Our methods are formal and rapid in nature since the automatically generated cycle-accurate simulator, the FSM RTL model and the test benches are extracted from the internal formally Synthesized state schedule models, after the optimization phase is concluded. A large number of benchmarks and real-life applications, were synthesized and verified with the discussed method and in all cases the formal methods caught specification or functional bugs early in the design flow, allowing the rapid implementation of the products.

Software product lines are increasingly used to handle the growing demand of custom-tailored software variants. They provide systematic reuse of software paired with variability mechanisms in the code to implement whole product families rather than single software products. A common domain of application for product lines are safety-critical systems, which require behavioral correctness to avoid dangerous situations in-field. While most approaches concentrate on post-hoc verification for product lines, we argue that a stepwise approach to create correct programs may be beneficial for developers to manage the growing variability. Correctness-by-construction is such a stepwise approach to create programs using a set of small, tractable refinement rules that guarantee the correctness of the program with regard to its specification. In this paper, we propose the first approach to develop correct-by-construction software product lines using feature-oriented programming. First, we extend correctness-by-construction by two refinement rules for variation points in the code. Second, we give a proof for the soundness of the proposed rules. Third, we implement our technique in a tool called VarCorC and show the applicability of the tool by conducting two case studies.

Proof assistants like Coq, Lean, or HOL4 rely heavily on stateful meta-programs called scripts to assemble proofs. Unlike pen-and-paper proofs, proof scripts only describe the steps to take (induct on x, apply a theorem, …), not the states that these steps lead to; as a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive user interface able to run the script and show the corresponding proof states. Until now, the standard process to communicate a proof without forcing readers to execute its script was to manually copy-paste intermediate proof states into the script, as source code comments — a tedious and error-prone exercise. Additional prose (such as for a book or tutorial) was likewise embedded in comments, preserving executability at the cost of a mediocre text-editing experience. This paper describes a new approach to the development and dissemination of literate proof scripts, with a focus on the Coq proof assistant. Specifically, we describe two contributions: a compiler that interleaves Coq’s output with the original proof script to produce interactive webpages that are complete, self-contained presentations of Coq proofs; and a new literate programming toolkit that allows authors to switch seamlessly between prose- and code-oriented views of the same sources, by translating back and forth between reStructuredText documents and literate Coq source files. In combination, these tools offer a new way to write, communicate, and preserve proofs, combining the flexibility of procedural proof scripts and the intelligibility of declarative proofs.

The rising popularity of the Internet-of-Things (IoT) devices has driven their increasing adoption in various settings, such as modern homes. IoT systems integrate such physical devices with third-party apps, which can coordinate in arbitrary ways. However, malicious or undesired coordination can lead to serious vulnerabilities. This paper explores two different ways, i.e., a commonly-used state-based approach and a holistic, rule-based approach, to formally model app coordination and the safety and security thereof in the context of IoT platforms. The less common rule-base approach allows for a smaller, more scalable model. We realize both modeling approaches using bounded model checking with Alloy to automatically identify potential cases where apps exhibit coordination relationships. We evaluate the effectiveness of the modeling approaches by checking a corpus of real-world IoT apps of Samsung SmartThings and IFTTT. The experimental results demonstrate that our rule-based modeling leads to a more scalable analysis.

Cyber-Physical System (CPS), which realizes the close integration of physical resources and information resources, is a distributed and asynchronous dynamic hybrid system running in different time and space. In this paper, we use AADL to model information system and use Modelica to model physical system. However, they are all semi-formal models such that we cannot do future work about formal verification. To overcome this defect, we convert them to formal models like automaton through conversion algorithms and rules. Due to the fact of probabilistic events and resource consumption in CPS, this paper adopts the weighted probabilistic hybrid automaton as formal model, and adds the properties of probability and weight to the behavior annex of AADL. Then we conduct the rule and algorithm of the model conversion. In order to ensure consistency of further work about model checking, the paper prove the equivalence of the two models by bisimulation. Finally, the capability of modeling of the extended modeling language of AADL and the significance of conversion to automaton is illustrated by the aircraft system.

Verification of cryptographic protocols is an urgent and complex task. In view of the development of various e-commerce services, as well as mobile robots, unmanned aerial vehicles, internet of things, in which computing resources are in most cases very limited and it is not always possible to use well-known protocols. Any developed protocol must go through a verification procedure. Mostly formal verification methods are used to evaluate the security of the cryptographic protocol. If the protocol has successfully vitrificated, it is implemented in the selected programming language for the developed system. Even though the protocol was successfully analyzed using formal verification tools, its implementation may be vulnerable. Errors may occur due to the human factor or protocol can be modified during implementation. Thus, the verification of cryptographic protocols source codes is relevant. The paper describes a dynamic analysis method for detecting replay-attacks and integrity violations.

Verification approaches based on constraint solvers are successfully applied in firmware and other low-level code that interfaces with hardware. While for proving safety of gate-level sequential circuits, it often suffices to bit-blast and reduce to SAT-based IC3 or Property Directed Reachability (IC3/PDR), for handling machine-level instructions that perform arithmetic and data manipulation operations, word-level reasoning should be conducted. However, because of poor support for interpolation and quantifier elimination in the theory of bit-vectors (BV), previous attempts to lift IC3/PDR to word level required integrating it into an external abstraction-refinement loop. Aiming to reach more scalable bit-precise verification, we propose to bring useful insights from PDR-based verification algorithms used in software. In particular, instead of using bit-blasting to eliminate quantifiers from BV-formulas, we present a less expensive method for iterative approximate quantifier elimination in BV. It naturally supports all bit-operators and can be optimized further by applying rules inspired by modular linear arithmetic. Finally, we leverage recent techniques on learning inductive invariants based on explicit global guidance, thus allowing the approach to bypass interpolation. Our implementation on top of Spacer, a PDR-based verifier shows that such a word-level PDR is promising and can be more effective than state-of-the-art.

Autonomous systems are self-governed and self-adaptive systems that must additionally comply with high assurance correctness and safety criteria. Such autonomous systems cannot be tested and verified in the traditional design process. While all systems hardware and software components can be implemented as usual, test and verification only cover the autonomous system functionality, but do not include the goal-driven autonomous behavior in all possible circumstances. This autonomous behavior is a primary design target. Thus, autonomous systems pose a number of emerging challenges and opportunities to the field of electronic design automation (EDA). Examples include specification of (evolving) requirements involving components and their interaction, defining different assurance levels for bounded operational environments, synthesis of mechanisms to guideline diagnosis and rigorously monitor systems integration after deployment.

We investigate whether modern messaging apps achieve the strong post-compromise security guarantees offered by their underlying protocols. In particular, we perform a black-box experiment in which a user becomes the victim of a clone attack; in this attack, the user's full state (including identity keys) is compromised by an attacker who clones their device and then later attempts to impersonate them, using the app through its user interface. Our attack should be prevented by protocols that offer post-compromise security, and thus, by all apps that are based on Signal's double-ratchet algorithm (for instance, the Signal app, WhatsApp, and Facebook Secret Conversations). Our experiments reveal that this is not the case: most deployed messaging apps fall far short of the security that their underlying mechanisms suggest. We conjecture that this security gap is a result of many apps trading security for usability, by tolerating certain forms of desynchronization. We show that the tolerance of desynchronization necessarily leads to loss of post-compromise security in the strict sense, but we also show that more security can be retained than is currently offered in practice. Concretely, we present a modified version of the double-ratchet algorithm that tolerates forms of desynchronization while still being able to detect cloning activity. Moreover, we formally analyze our algorithm using the Tamarin prover to show that it achieves the desired security properties.

International audience; Models have been shown to be useful during virtually all stages of the software lifecycle. They can be reverse engineered from existing artifacts, or created as part of a system’s execution, but in many cases models are created by designers from informal specifications. In the latter case, such design models are typically used as means of communication between designers, and developers. They can also in some cases be validated by simulation over test cases, or even by formal verification. However, most existing model simulation or verification approaches require relatively consistent and complete models, whereas design models often start small, incomplete, and inconsistent. Moreover, few design models actually reach the stage where they can be simulated, and even fewer the stage where they can be formally verified. In order to address this issue, we propose a partial modeling approach that makes it possible to animate incomplete and inconsistent models. This approach makes it possible to incrementally improve testable models, and can also help designers reach the stage where their models can be formally verified. A proof-of-concept tool called AnimUML has been created in order to provide means to evaluate the approach on several examples. They are all executable, and some can even undergo model-checking.