ABSTRACT. Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages. In this talk, we will see how to design secure electronic voting protocols and how to analyze them using formal methods, in order to detect attacks at an early stage, or prove security. This yielded several enhancements of ProVerif, a state-of-the-art tool for anaysing security protocols.

ABSTRACT. Proving theorems and properties on B models, recursively-defined functions is a convenient tool which is missing in B proofs. The main contribution of this paper is the definition of a new theory without new concrete types and without axioms to enable the use of constructions by induction; This theory has been specified and proved within the Theory Plugin in Rodin. This induction theory clearly improves the existing B prover. This is illustrated in this paper by the implementation of ZFC in the Theory Plugin.

ABSTRACT. The TLAPS proof assistant for TLA+ sends proof obligations to external automated provers, including SMT solvers. It features an encoding of TLA+ into SMT-LIB, but the current implementation of this encoding is complex and its soundness is hard to ensure. We present a new, simpler encoding for SMT that is based on a first-order axiomatization with E-matching patterns. We implemented the encoding in TLAPS and evaluated it on specifications from the TLA+ distribution.

ABSTRACT. Event-B is a state-based correct-by-construction system design formal method relying on proof and refinement where system models are expressed using set theory and FOL. Through the generation and discharging of proof obligations (POs), Event-B natively supports the establishment of properties such as safety invariant, convergence and refinement (trace simulation). Other properties, relevant to system verification (deadlock-freeness, reachability, liveness) may be studied as well, but need to be explicitly formalised by the designer, or expressed in another formal method. This process compromises reusability and is error-prone, especially on larger systems. Recently, the EB4EB framework formalises, in Event-B, each Event-B concepts as first-class objects, making it possible to manipulate them in Event-B using FOL and set theory.

In this paper, we propose a rigorous methodology for extending the EB4EB framework, to support new system analysis mechanisms associated to properties that are not natively present in core Event-B. Thanks to the reflexive nature of this framework, new generic and reusable system properties and their associated POs are expressed once and for all, and for any refinement level. For specific systems, designers instantiate these properties and the associated POs are automatically generated and submitted to Event-B's provers. This methodology is used to define three analyses: deadlock-freeness, invariant weakness analysis and reachability, all of which are demonstrated on a case study.

ABSTRACT. Records are a basic composite data type available in most programming and specification languages, but which are not natively supported by Alloy due to its semantics purely based on relational logic. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures.

This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy's flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge of the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms.

ABSTRACT. In the design of critical systems, it is important to ensure a degree of formality so that we reason about safety and security at early stages of analysis and design, rather than detect problems later. Influenced by ideas from STPA we present a hierarchical analysis process that aims to justify the design and flow-down of derived critical requirements arising from safety hazards and security vulnerabilities identified at the system level. At each level, we verify that the design achieves the safe- ty/security requirements by backing the analysis with formal modelling and proof using Event-B refinement. The formal model helps to identify hazards/vulnerabilities arising from the design and how they relate to the safety accidents/security losses being considered at this level. We then re-apply the same process to each component of the design in a hierarchical manner. Thus we use ideas from STPA, backed by Event-B models, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical requirements down to components, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards/vulnerabilities are eliminated.

ABSTRACT. This ``journal-first'' paper presents a summary of the behavioural theory of reflective sequential algorithms (RSAs), i.e.\@ sequential algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates defining the class of RSAs, an abstract machine model, and the proof that all RSAs are captured by this machine model. RSAs are sequential-time, bounded parallel algorithms, where the bound depends on the algorithm only and not on the input. Every state of an RSA includes a representation of the algorithm in that state, thus enabling linguistic reflection. Bounded exploration is preserved using terms as values. The model of reflective sequential abstract state machines (rsASMs) extends sequential ASMs using extended states that include an updatable representation of the main ASM rule to be executed by the machine in that state. Updates to the representation of ASM signatures and rules are realised by means of a tree algebra.

ABSTRACT. This ``journal-first'' paper summarises a publication by the same authors in the journal Logical Methods in Computer Science which describes a formal semantics for the Event-B specification language using the theory of institutions. It defines an institution for Event-B and shows how the constructs of the Event-B specification language can be mapped into our institution. This algebraic semantics distinguishes three constituent sub-languages of Event-B: the superstructure, infrastructure and mathematical languages. An important impact of this work is that our semantics provides access to the generic modularisation constructs available in institutions, including specification-building operators for parameterisation and refinement. We demonstrate how these features subsume and enhance the corresponding features already present in Event-B through a detailed study of their use in a worked example. Further benefits of the institutional approach are its provision for mathematically definable interoperability to facilitate heterogeneous specification.

ABSTRACT. Recently, a behavioural theory for reflective algorithms has been developed, which shows that reflective (sequential) ASMs (rASMs) capture all reflective (sequential) algorithms. In this paper we explore the expressive power of rASMs for genetic algorithms and security. We first show that all genetic algorithms are captured by rASMs. Then we elaborate recombinative simulated annealing as a specific example of a genetic algorithm specified an rASM. We further show how rASMs can support copy protection, and we exploit the logic of rASMs to verify desirable properties for this application.

ABSTRACT. Hybrid dynamical systems describe the mixed discrete dy- namics and continuous dynamics of cyber-physical systems such as air- craft, cars, trains, and robots. To justify correctness of their safety- critical controls for their physical models, differential dynamic logic (dL) provides deductive specification and verification techniques implemented in the theorem prover KeYmaera X. The logic dL is useful for proving, e.g., that all runs of a hybrid dynamical system are safe ([α]φ), or that there is a run of the hybrid dynamical system ultimately reaching the desired goal (⟨α⟩φ). Combinations of dL’s operators naturally represent safety, liveness, stability and other properties. Variations of dL serve ad- ditional purposes. Differential refinement logic (dRL) adds an operator α ≤ β expressing that hybrid system α refines hybrid system β, which is useful, e.g., for relating concrete system implementations to their ab- stract verification models. Just like dL, dRL is a logic closed under all operators, which opens up systematic ways of simultaneously relating systems and their properties, of reducing system properties to system relations or, vice versa, reducing system relations to system properties. Differential game logic (dGL) adds the ability of referring to winning strategies of players in hybrid games, which is useful for establishing cor- rectness properties of systems where the actions of different agents may interfere. dL and its variations have been used in KeYmaera X for ver- ifying ground robot obstacle avoidance, the Next-Generation Airborne Collision Avoidance System ACAS X, and the kinematics of train con- trol in the Federal Railroad Administration model with track terrain influence and air pressure brake propagation.