fmsec

Formal Methods for Security Network


This a network of researchers and practitioners interested in formal methods for security, in theory, in tools and in the mix of both.

FM-SEC is born out of former “UK Network for Formal Methods in Security”, which was UK-based (see here).

FM-SEC is now a wider, international endavour. We run primarily as a seminar series, with monthly talks, by those active in and interested in formal methods for security.

We are co-hosting most of our events with the “Cyber Security & Privacy Seminar Series” (UK SPS); some events which are network-oriented or central to formal methods are hosted separately from UK SPS.

Current Talks

  • 28 June, 3PM UK time, Muhammad Usama Sardar, joint with UK SPS, Title: Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing
    <summary> Details(abstract):</summary>
    Abstract: Confidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs) has emerged as a promising solution for protecting sensitive data in all forms. One of the fundamental characteristics of such TEEs is remote attestation which provides mechanisms for securely measuring and reporting the state of the remote platform and computing environment to a user. We present a novel approach combining TEE-agnostic attestation architecture and formal analysis enabling comprehensive and rigorous security analysis of attestation mechanisms in CC. We demonstrate the application of our approach for three prominent industrial representatives, namely Arm Confidential Compute Architecture (CCA) in architecture lead solutions, Intel Trust Domain Extensions (TDX) in vendor solutions, and Secure CONtainer Environment (SCONE) in frameworks. For each of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism in confidential computing, namely provisioning, initialization, and attestation protocol. Our approach reveals design and security issues in Intel TDX and SCONE attestation. The talk is based on joint work with Thomas Fossati and Simon Frost from Arm.

Zoom mtg: 962 3227 7992; passcode 856952; link here

Youtube link here

Past Talks

  • 24 May, 3PM UK time, Fulvio Valenza, joint with UK SPS, Title: Formal and Automatic Network Security Configuration

    <summary> Details(abstract):</summary>
    Abstract: The next-generation networks introduced higher flexibility and dynamicity in networking systems, but at the same time, they led to new threats and challenges. The traditional approach of a manual configuration of Network Security Functions (NSFs) such as firewalls and VPN gateways is not feasible anymore since it is not adequate for the ever-changing nature of modern networks and it is prone to human errors. To overcome this problem, the native flexibility provided by virtualization could be exploited to automate network security management. However, achieving a high level of automation while providing formal assurance that security management operations (e.g., configuration and orchestration) fulfill some security properties is still a complex research challenge. This presentation describes some novel approaches that combine automation, formal verification, and optimization for network security management.

  • 22 March, 3PM UK time, Francois Dupressoir, joint with UK SPS, Title: EasyCrypt in anger — Proofs for Primitives, Constructions and Protocols

    Details (abstract):
    Abstract: The EasyCrypt proof assistant offers—in a single tool—the ability to reason about cryptographic security at various scales from primitives to protocols. However, this flexibility comes at a huge cost in usability. This talk will discuss insights gained through the recent formalisation of primitives (SHA-3, XMSS), constructions (KMS, crypto_box) and protocols (distance-bounding, AKE) and explore plans for improvements to the tool that would enable its use on larger protocols, and for the creation of beginner-friendly tutorial material that would enable it to be used more broadly.

See on Youtube here

  • 18 Jan, 3PM UK time, Jam Ramanujam, joint with UK SPS, Title: Insecurity, going from terms to formulas
    Details (abstract):
    Abstract: Reasoning about cryptographic protocols starts with a term algebra of communicated terms over which an appropriate logic is built, with variables designating terms. In logics of announcements, formulas are communicated, blurring the distinction between terms and formulas. Constructs such as zero knowledge proofs and certificates are akin to formulas, motivating a similar extension to reasoning about security protocols as well. However, the interaction between equality and the existential quantifier leads to interesting twists: witnesses for existential quantifiers may be unbounded, and obtaining small witness terms while maintaining equality proofs complicates the analysis considerably. In this talk we attempt to highlight the challenges in reasoning about insecurity when formulas are communicated. This work is joint with Vaishnavi Sundararajan and S P Suresh.

See on Youtube: here

  • 11 Jan, 3PM UK time, Tom Chothia, joint with UK SPS, Title: Blackbox and Grey-box Approaches to Protocol State Machine Learning (With Lots of Attacks Against TLS and WPA)
    Details (abstract):
    Protocol state machine learning has been used to analyse many cryptographic protocols. Unlike fuzzing it can find logical flaws in protocols and unlike formal modelling it can find vulnerabilities in implementations. I will outline how black box state machine methods work, and describe how we have applied them to WPA to find two downgrade attacks. I will then describe a grey box learning method we have developed that uses memory snapshots and symbolic execution of the binary, combined with observations of run-time memory and a protocol’s inputs and outputs to learn its state machine. We show that this grey box method is much more efficient than black box learning, allowing us to test protocols in much more detail and leading to the discovery of new attacks against implementations of TLS and WPA. This is joint work with: Chris McMahon Stone, Sam L. Thomas, Joeri de Ruiter, Mathy Vanhoef, James Henderson and Nicolas Bailluet

See on Youtube: here

  • 30 November, 3PM UK time, Alexandre Debant, joint with UK SPS, Title: Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol
    Details (abstract):
    In June 2022, French citizens abroad voted online during the French legislatives election to chose the new members of Parliament. In this work, we conducted a security analysis of the system under use. Due to a lack of system and threat model specifications, we first built and contributed such specifications by studying the French legal framework and by reverse-engineering the code base accessible to the voters. Our analysis reveals that this protocol is affected by two design-level and implementation-level vulnerabilities. We show how those allow a standard voting server attacker and even more so a channel attacker to defeat the election integrity and ballot privacy. We propose and discuss fixes to prevent those attacks. Our specifications, the attacks, and the fixes were acknowledged by the relevant stakeholders during our responsible disclosure. Beyond this specific protocol, we draw general conclusions and lessons from this instructive experience where an e-voting protocol meets the real-world constraints of a large-scale and political election.

See on Youtube: here

  • 19 October, 3PM UK time, Pascal Lafourcarde, joint with UK SPS, Title: (In)Security of e-exams
    Details (abstract):
    In this talk I will present our works on e-exams. We have proposed a formal framework for e-exams. In this context we have been able to define several security properties. Some of these properties have been checked on existing protocols of the literature using automatic tools like Proverif.

See this on Youtube: here

  • 21 September, 3PM UK time, Steve Kremer, joint with UK SPS, Title: Symbolic protocol verification with dice: process equivalences in the presence of probabilities
    Details (abstract):
    Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has-maybe surprisingly-a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity. This is joint work with Vincent Cheval and Raphaëlle Crubillé.

See this on Youtube: here

  • 20 July, 3PM UK time, Charlie Jacomme, joint with UK SPS, Title: Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol.
    Details (abstract):
    Abstract : We believe that formal methods in security should be leveraged in all the standardisation's of security protocols in order to strengthen their guarantees. To be effective, such analyses should be: * maintainable: the security analysis should be performed on every step of the way, i.e. each iteration of the draft; * pessimistic: all possible threat models, notably all sort of compromise should be considered; * precise: the analysis should notably include as many real life weaknesses of the concrete cryptographic primitives specified. In this talk, we illustrate how such a goal may be approached by detailing our analysis of the current IETF draft standard of the EDHOC protocol, as well as our subsequent interactions with its LAKE working group. We will proceed in three steps, first introducing the Sapic+ platform that allows from a single modeling of a protocol to benefit from all the capabilities of multiple automated verification tools (ProVerif,Tamarin,DeepSec). We will then introduce multiple recent advances on how to better model the cryptographic primitives and their real life weaknesses. We will finally show how we leveraged Sapic+ along with the advanced primitive models to analyze the EDHOC protocol and provide feedback to the LAKE working group that has been integrated in latter drafts.

See this on Youtube: here

  • 29 June, 3PM UK time, Vincent Cheval, joint with UK SPS, Title: A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
    Details (abstract):
    Abstract : ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction. In the original paper of GSVerif, our key idea was to devise a generic transformation of the security properties queried to ProVerif. We proved the soundness of our transformation and implemented it into a front-end GSVerif. Our experiments showed that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully applied our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature. In the newest version of ProVerif, the generic transformations of GSVerif can be fully described in term of axioms, thus taking advantage of this new ProVerif feature.

See this on Youtube: here

  • 18 May, 3PM UK time, Bruno Blanchet, joint with UK SPS, Title: The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more.
    Details (abstract):
    Abstract: ProVerif is a widely used automatic security protocol verifier that relies on symbolic model of cryptography. It can prove various security properties (secrecy, correspondences, some equivalences) for an unbounded number of sessions, as well as find attacks. In this talk, we will present an overview of ProVerif and its recent improvements. These improvements are twofold. First, we extended ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we reworked and optimized many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, ...), resulting in impressive speed-ups on large examples. These improvements are joint work with Vincent Cheval and Véronique Cortier, to appear at IEEE Security and Privacy 2022.

See this on Youtube: here

  • 13 April, 3PM UK time, Musard Balliu, joint with UK SPS, Title: Securing Cloud-based IoT Apps.
    Details (abstract):
    Abstract: Innovative IoT apps break conventional paradigms to connect otherwise unconnected services and devices ranging from pacemakers, baby monitors, surveillance cameras to cars and smart cities. Unfortunately, the power of IoT apps can be abused by attackers, unnoticeably to users. In this talk, we will discuss how popular IoT app platforms are susceptible to attacks that violate user privacy resulting in massive exfiltration of sensitive information as well as suggest short- and long-term countermeasures based on language-based sandboxing and information flow control.

See this on Youtube: here

Managed by

Ioana Boureanu and Erisa Karafili

What to Join or Give a Talk? Email us at fmsecresearch@gmail.com