ABSTRACT. More and more software systems, including in the critical industry,  exploit concurrency and multi-core architectures. Verifying concurrent  systems is challenging due to the huge number of possible executions  spawned by the (inherently highly non-deterministic) scheduler. Yet,  sound analyses covering all possible executions are necessary to  certify software and discover subtle concurrency bugs.
In this talk, we present several static analyses of such systems that  avoid considering explicitly all possible thread interleavings, and  use instead thread-modular techniques: we analyze separately each  thread as well as their interactions, performing a fixpoint to  propagate interactions between threads. The methods are based on  abstract interpretation, which ensures soundness by construction and  allows a wide range of cost versus precision trade-offs while  leveraging for free all the abstractions developed to analyze  sequential programs.
We present several analyses built on this model, including: an  extension to concurrent programs of the Astrée analyzer to prove the  absence of run-time errors in embedded critical C code, an analysis of  the functional correctness of device drivers in TinyOS, and an  analysis inferring numeric invariants in low-level concurrent programs  in the presence of weak hardware memory consistency models.

ABSTRACT. Open pNets are used to model the behaviour of open systems, both synchronous or asynchronous, expressed in various calculi or languages. They are endowed with a symbolic operational semantics in terms of so-called “Open Automata”. This allows to check properties of such systems in a compositional manner. We implement an algorithm computing this semantics, building predicates expressing the synchronization conditions between the events of the pNet sub-systems. Checking such predicates requires symbolic reasoning over first order logics, but also over application-specific data. We use the Z3 SMT engine to check satisfiability of the predicates, and prune the open automaton of its unsatisfiable transitions. As an industrial oriented use-case, we use so-called "architectures" for BIP systems, that have been used in the framework of an ESA project and to specify the control software of a nanosatellite at the EPFL Space Engineering Center. We use pNets to encode a BIP architecture extended with explicit data, and compute its open automaton semantics. This automaton may be used to prove behavioural properties; we give 2 examples, a safety and a liveness property.

ABSTRACT. There is a strong link between software quality and software reliability. By decreasing the probability of imperfection in the software, we can augment its reliability guarantees. At one extreme, software with one unknown bug is not reliable. At the other extreme, perfect software is fully reliable. Formal verification with SPARK has been used for years to get as close as possible to zero-defect software. We present the well-established processes surrounding the use of SPARK at Altran UK, as well as the deployment experiments performed at Thales to fine-tune the gradual insertion of formal verification techniques in existing processes. Experience of both long-term and new users helped us define adoption and usage guidelines for SPARK based on five levels of increasing assurance that map well with industrial needs in practice.

ABSTRACT. Modern railway stations are controlled by computerized systems called interlockings. In fact the middle size and large size stations usually required to use several interlockings then forming a network. Many researches propose to verify the safety properties of such system by mean of model checking. Our approach goes a step further and proposes a method to extend the verification process to interconnected interlockings. This process is known as compositional verification. Each interlocking is seen as the component of a larger system (i.e.; station) and interacts with its neighbours by mean of interfaces. Our first contribution comes in the form of a catalogue of formal definitions covering all the interfaces used by the Belgian Railways. Each interface can then be bound to a formal contract allowing its verification by the ocra tool. Our second contribution is to propose an algorithm able to split the topology controlled by a single interlocking into components. This allows to reduce the size of the model to be verified thereby reducing the state space explosion while providing guarantees on the whole interlocking.

ABSTRACT. SPARK is a technology for mathematically proving that programs are correct, that has completed its 30th birthday in 2017, making it one of the oldest such technology alive! Its longevity can be explained by a stubborn focus on the development of tools usable by software engineers and applicable to industrial software. The "tools" include here a programming language, development and verification tools, and processes around these. These tools have evolved considerably in three decades, with even a complete overhaul between 2010 and 2014 to unify the logical and executable views of specifications. We are seeing now adoption progressing at a faster rate, mostly because the level of automation has decreased entry costs for users. Normal engineers can start proving the correctness of their programs on their personal computers. An apparent paradox is that program proving itself, understood as the full functional correctness of programs, is not much easier today. What is much easier thanks to automation however is the proof of simpler yet critical properties of programs, like the absence of runtime errors. An unavoidable consequence is that, as engineers try to prove more complex properties on their programs, automation is not the panacea. We tell them: Don't Panic! SPARK offers a continuum from automatic proof to interactive proof, allowing users to decide where to set the target of their journey. In this talk, we will provide the hitchhiker's guide to the SPARK proof galaxy.

ABSTRACT. Software-defined networks (SDN) offer a high degree of programmability for handling and forwarding packets. In particular, they allow network administrators to combine different security functions, such as firewalls, intrusion detection systems, and external services, into security chains designed to prevent or mitigate attacks against end user applications. Because of their complexity, the configuration of these chains can benefit from formal techniques for their automated construction and verification. We propose in this paper a rule-based system for automating the composition and configuration of chains of security functions for Android applications. Given a characterization of the network traffic generated by an application and the set of permissions it requires, our rules construct an abstract representation of a custom security chain. This representation is then translated into a concrete implementation of the chain in Pyretic, a domain-specific language for programming SDN controllers. We prove that the chains produced by our rules satisfy a number of correctness properties such as the absence of black holes or loops, and shadowing freedom, and that they are coherent with the underlying security policy.

ABSTRACT. The development of provably secure OS kernels represents a fundamental step in the creation of safe and secure systems. To this aim, we propose the notion of protokernel and an implementation --- the Pip protokernel --- as a separation kernel whose trusted computing base is reduced to its bare bones, essentially providing separation of tasks in memory, on top of which non-influence can be proved. This proof-oriented design allows us to formally prove separation properties on a concrete executable model very close to its automatically extracted C implementation. Our design is shown to be realistic as it can execute isolated instances of a real-time embedded system that has moreover been modified to isolate its own processes through the Pip services.