Formal verification is the mathematical proof of the correctness of algorithms, protocols and computer systems. In the last decades proof assistants like Isabelle have verified a general-purpose operating system microkernel in the order of 10000 lines of C-code as well as a 300-pages textbook on programming language semantics. Journals like Archive of Formal Proof has numerous verified articles covering both mathematics and computer science topics and many other verification projects have been successfully completed. The development and use of proof assistants and related tools, including model checking and advanced solvers, can be found in several sections at DTU Compute, for example in analysis of embedded systems, software specification and verification, security protocols, algorithms and meta-logic. The aim of the project is to strengthen the cross-sectional cooperation in formal verification research and teaching.
Tuesday 28 February 2017 - DTU room 101/S16 10:15-10:30 John Bruntse Larsen & Jørgen Villadsen: An Approach for Hospital Planning with Multi-Agent Organizations 10:30-11:30 Virginia Dignum (TU Delft, The Netherlands): Interactions as Social Practices - Towards a Formalization
Abstract for the talk by Virginia Dignum: Multi-agent modelling and simulation are a suitable starting point to model complex social interactions. However, as the complexity of the systems increase, we argue that novel modelling approaches are needed that can deal with inter-dependencies at different levels of society, where many heterogeneous parties are interacting and reacting to each other. We argue that for many intelligent and autonomous systems the BDI (Belief-Desire-Intention) architecture is a solid basis, but does not give enough support to model the autonomous decision processes required for these systems. In this talk, we sketch a fundamentally social formal framework for the agents in these simulations in order to get a grip on the underlying mechanisms at work. We show some scenarios where we applied some of the ideas and sketch the sociological foundation of the agents and an agent architecture that can be used for building agent based simulations for societal challenges.
All are welcome. Registration is not necessary.
Organizers: Michael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander Mödersheim and Jørgen Villadsen (DTU Compute)
Supported by DTU Compute's Strategic Foundation
Wednesday 30 November 2016 - DTU room 325/H009 9:30-10:15 Achim Brucker: Security of Browser Extensions - Towards a Formal Model 10:45-11:30 Christoph Sprenger: Refining Authenticated Key Agreement with Strong Adversaries 13:00-13:45 Andrei Popescu (joint work with Ondrej Kuncar): A Consistent Foundation for Isabelle/HOL 14:15-15:00 Heinrich Ody: Discounted Duration Calculus 15:30-16:15 Markus Roggenbach: On the 'Algebra' of Railway Interlockings 16:15-17:00 Hugo Daniel dos Santos Macedo: Compositional Verification of Multi-Station Interlocking Systems
Achim Brucker (University of Sheffield, UK): Security of Browser Extensions - Towards a Formal Model
On the one hand, browser extensions, e.g., for Chrome, are very useful, as they extend web browsers with additional functionality (e.g., blocking advertisements). On the other hand, they are the most dangerous code that runs in your browsers: extension can modify both the content displayed in the browser as well as the communication with any web-site or web-service. Moreover, the current security model for browser extensions seems to be inadequate for expressing the security and privacy needs of browser users. Consequently, browser extensions are a "juice target" for attackers targeting web users. In this talk, we first present our results of analyzing the current security model of browser extensions. Second, we present first steps towards formally modeling the parts of a web browser that are necessary to analyze and propose a future security model for browser extensions. The long-term goal of our work is to provide a formally verified security model for web browser extensions that focuses on the need of browser users.
Christoph Sprenger (ETH Zurich, Switzerland): Refining Authenticated Key Agreement with Strong Adversaries
This talk presents the development of a family of key agreement protocols that are correct-by-construction. Our development method is based on stepwise refinement. We use our previously proposed refinement strategy, which transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style adversary. As intermediate levels of abstraction, we employ message-less guard protocols and channel protocols communicating over channels with security properties. The present work substantially extends this framework. First, we strengthen the adversary by allowing him to compromise different resources of protocol participants, such as their long-term keys or their session keys. This enables the systematic development of protocols that ensure strong properties such as perfect-forward secrecy. Second, we broaden the class of protocols supported to include those with non-atomic keys and equationally defined cryptographic operators. Third, we implement channels in a parametric way, under a set of assumptions that any concrete implementation must satisfy. This approach sheds light on the conditions that are needed for such implementations to be secure and makes security proofs more modular. These extensions required a major redesign of our previous framework. We have implemented our method in Isabelle/HOL and used it to develop key agreement protocols including signed Diffie-Hellman and the core of IKEv1 and SKEME.
Andrei Popescu (Middlesex University London, UK): A Consistent Foundation for Isabelle/HOL (joint work with Ondrej Kuncar)
The interactive theorem prover Isabelle/HOL is based on the well understood Higher-Order Logic (HOL), which is widely believed to be consistent (and provably consistent in set theory by a standard semantic argument). However, Isabelle/HOL brings its own personal touch to HOL: overloaded constant definitions, used to achieve Haskell-like type classes in the user space. These features are a delight for the users, but unfortunately are not easy to get right as an extension of HOL—they have a history of inconsistent behavior. It has been an open question under which criteria overloaded constant definitions and type definitions can be combined together while still guaranteeing consistency. This paper presents a solution to this problem: non-overlapping definitions and termination of the definition-dependency relation (tracked not only through constants but also through types) ensures relative consistency of Isabelle/HOL.
Heinrich Ody (Carl von Ossietzky Universität Oldenburg, Germany): Discounted Duration Calculus
To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.
Markus Roggenbach (Swansea University, UK): On the 'Algebra' of Railway Interlockings
Formal verification of railway control software has been identified as one of the "grand challenges" of Computer Science. This challenge comes in two parts. The first addresses the question of whether proposed mathematical models faithfully represent the railway domain; verifications must translate to guarantees in the real world. The second addresses the question of how to employ available technologies effectively; analyses must be doable in practice and not just in theory. Our talk will focus on the second, while briefly touching on the first of these challenges. In addressing the second part of the grand challenge we face the wider challenge for formal methods of overcoming state space explosion. Having rendered a real-world problem into a modelling language, it remains a mystery in general as to how to decompose a verification problem into tractable pieces whose solutions can be composed together to provide a solution to the initial problem. Our approach is to carry out abstractions at the domain level, thus avoiding the lack of general compositional techniques in modelling languages. We have developed three abstraction techniques which provide - to a certain extent - the 'algebraic' laws of railway interlockings. These techniques have proven successful in practice, both in isolation and taken together: 1. Finitisation reduces the number of trains that need to be considered in order to prove safety for an unbounded number of trains; 2. Covering decomposes the network into a set of sub-networks in a compositional fashion: proving correctness results for the sub-networks suffices to infer the correctness of the whole network; and 3. Topological abstraction reduces the number of tracks in the topology of the network, so as to minimise the size and complexity of the network prior to its analysis. The second abstraction technique is a particular strength of our approach. In her 2003 paper, Winter theorized on the possibility of such compositional proof strategies for the railway domain, but to our knowledge there has since been no practical solution. Putting things into the wider context of a "grand challenge" again, our work in the railway domain might serve as witness for our belief: careful analysis on the domain level will lead to the abstractions and decompositions which are key to the successful application of Formal Methods on industrial size challenges.
Hugo Daniel dos Santos Macedo (DTU Compute): Compositional Verification of Multi-Station Interlocking Systems
The railway controlling interlocking systems are safety-critical components and their automated safety verification is an active research topic involving several groups that typically employ verification techniques to produce important cost and time savings in their certification. Such systems pose a big challenge to general verification tools due to the inherent computational resource demands. In this talk we report on how we improve an existing tool to verify models of the new Danish interlocking systems by exploring the locality principles related to the topological layout of the controlled system.
Wednesday 20 April 2016 - DTU room 101/S09 9:15-9:30 Jørgen Villadsen & Sebastian Alexander Mödersheim: Welcome / The PART Project 9:30-10:00 Burkhart Wolff (Université Paris-Sud, France): Experiences of a Formal Certification Project EURO-MILS - Why is it so hard to get proofs accepted in Common Criteria Projects 10:00-10:30 Burkhart Wolff: Parallel Computing in an Interactive Theorem Prover - Experiences from the Paral-ITP Project 11:00-12:00 Tom Ridge (University of Leicester, UK): Netsem, Ott, Lem, SibylFS and Verified Parsing: Specification and Validation at Scale 13:00-13:45 Carsten Schürmann (ITU): Specifying Security Protocols in Celf 14:00-14:30 Jørgen Villadsen & Anders Schlichtkrull: Computer-Checked Logical Inference Systems 14:30-15:00 Sebastian Alexander Mödersheim & Andreas Viktor Hess: Proving Protocol Security in Isabelle: Towards State and Composition
Abstract for the talk by Tom Ridge: I have worked on several large specification and validation projects (those mentioned in the title), and tools to support these projects. Most recently, the SibylFS project (sibylfs.io) gave a formal semantics to POSIX and real-world file systems. The semantics was extensively validated, which uncovered numerous bugs and strange behaviours in real-world file systems and the POSIX specification itself. Interestingly, we also found errors (at least one of which was serious) in a *formally verified file system*. In this talk I want to discuss these projects, particularly focusing on how they form a coherent body of work. I also want to explicitly state and analyse the assumptions that lie behind this work. Finally, I would like to discuss how I plan to extend this work in the future.
Wednesday 23 September 2015 - DTU room 101/S09 09:00-09:15 Jørgen Villadsen: Welcome / The PART Project 09:15-10:15 Alessandro Fantechi: How Formal Modeling Can Address Advanced Issues in Railway Signalling (break) 10:30-11:15 Anne Elisabeth Haxthausen: Combining Domain-specific Methods and Bounded Model Checking in the Railway Domain 11:15-11:45 Michael Reichhardt Hansen: Towards a Realizable Interpretation of a Logic for Traffic Analysis (lunch) 12:30-13:30 Jasmin C. Blanchette: Towards Formalizing Superposition 13:30-14:00 Anders Schlichtkrull: Formalization of Resolution Calculus in Isabelle 14:00-14:30 Mathias Fleury: Formalization of Ground Inference Systems in Isabelle Thursday 24 September 2015 - DTU room 101/S09 09:00-10:00 Martin Fränzle: Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems (break) 10:15-10:45 Jørgen Villadsen: Using the Isabelle Proof Assistant for Teaching Logic 10:45-11:15 Steen Vester: Winning Cores in Parity Games 11:15-11:45 Mathias Nygaard Justesen: A Verification Framework Using Parity Games (lunch) 12:30-13:30 Achim D. Brucker: Isabelle: Not Only a Proof Assistant 13:30-14:00 Sebastian Alexander Mödersheim: Automated Security Proofs in Isabelle 14:00-14:30 Alessandro Bruni: Proving Stateful Injective Agreement with Refinement Types
12:00-12:05 Opening session
12:15-12:45 Jørgen Villadsen (DTU Compute): Computer-Checked Meta-Logic
Abstract: Over the past decades there have been several impressive results in computer-checked meta-logic, including the correctness of proof systems for first-order and higher-order logic as well as the first-ever formalization of Gödel's Incompleteness Theorems, recently published by Larry Paulson as a 250+ pages document for the Isabelle proof assistant. I give a brief overview of the research area and discuss the prospects for verified and self-verified systems.
13:00-13:30 Jesper Bengtson (ITU): Software Verification Using Proof Assistants
Abstract: Proving full functional correctness of software has long been a holy grail for computer scientists. To be able to ease up on testing and also verify that a program follows its specifications to the letter, that no corner case has been overlooked and that no stone has been left unturned, is an exhilarating concept. To realise this goal three things are required. First of all, we must have a specification language that is rich enough to express all properties of programs that we are interested in. Secondly, since proofs of program correctness are typically very large we need a tool that automates as much of the process as possible, provides interactive support when it is not, and ensures that all proofs are valid and that no mistakes have been made. Finally, the verification process needs to find its way into the standard IDEs that are part of the system developers work flow. In this talk I will focus on my work to tackle these three goals by (1) using higher-order separation logic to write specifications for imperative object-oriented programming languages, (2) mechanising these logics in the interactive proof assistant Coq, and (3) developing a verification environment as a plugin for the Java development environment of Eclipse. The talk will be at a high level of abstraction and no expertise in either of these areas is required.
14:00-14:30 Sebastian Alexander Mödersheim (DTU Compute): Integrating Automated and Interactive Protocol Verification (joint work with Achim Brucker, SAP Research)
Abstract: Several automated protocol verification tools are based on an over-approximation of the set of possible traces. The underlying protocol models are shaped by the needs of automated verification and have subtle assumptions. Also, a complex verification tool may suffer from implementation bugs. Thus, in the worst case a tool could accept some incorrect protocols as being correct. The same risks are also present, but considerably smaller, when using an LCF-style theorem prover like Isabelle. The interactive security proof, however, requires a lot of expertise and time. We look at two approaches that combine the advantages of both worlds, by using automatic tools to generate a "proof idea" for an interactive theorem prover. In the worst case (e.g., a bug) this proof idea will simply not check out in the theorem prover. However, when it succeeds, the correctness only relies on the basic model and the correctness of the "core" of the theorem prover.
14:45-15:15 Ximeng Li (DTU Compute): Coq for Programming Language Proofs - A Personal Experience
Abstract: This talk is centered around a personal experience on using Coq to develop proofs for a draft paper on information flow security. Instrumented semantics is used to capture the flows arising from computation, and a type system then guarantees that only secure flows are admitted. The Coq development consists of the formulation of the syntax of a simple concurrent language, its instrumented semantics, the security type system, and a soundness result. The development uses mostly elementary to intermediate features of the Coq language and some excerpts of it will be displayed and discussed.
15:30-16:00 Closing session
Jørgen Villadsen 2017-02-24 http://part.compute.dtu.dk/