Tutorials and Keynotes

Tutorials

The tutorials will take place on 2 October, 2017.

Shin’ichiro Matsuo (Georgetown University/CELLOS Consortium/BSafe.network)

How Formal Methods and Analysis Helps Security of Entire Blockchain-based Systems

Abstract: For long years, formal methods and formal analysis usually collect much attention in designing mechanisms, products and systems, to eliminating errors and troubles. Communication protocol and cryptographic protocol is one of the important area where formal analysis is applied to reduce the possibility of attacks and vulnerability. Currently we use many cryptographic protocols in our life and they are already fundamental of our communication. Recently, we are proceeding the next stage where cryptographic protocol acts a fundamental role of ecosystem. Bitcoin and Blockchain opens our eyes for decentralized ecosystem by combination of cryptographic protocol, P2P network and consensus algorithm. At this moment, the security of this well-balanced but complicated combination is not fully proven. Moreover, blockchain is a foundation of many applications and we should care about security of entire application and systems based on blockchain technology.

In this tutorial, we will study how formal analysis helps evaluating the security of entire blockchain based systems. We analyze the entire blockchain based system with dividing into 6 security layers, then explore the possibility of applying formal analysis to each layers with examples. We also discuss a way to securing smart contract, which is one of the most promising application of blockchain technology. Research on security of blockchain based system is in its quite early stage, therefore, we need more research on formal analysis theory and methodology. We will discuss the further research directions to securing next foundation of trust.

Cas Cremers, Oxford University

Symbolic Security Analysis using the Tamarin Prover

Abstract: In this talk I will present the Tamarin Prover, an analysis tool for symbolic security analysis of systems. A prime example of systems that fall within its scope are security protocols that are executed in the presence of an active attacker. Tamarin’s state-of-the-art analysis of such systems requires dealing with unbounded replication of processes, loops, the prolific behaviour of the attacker, and equational theories to model cryptographic operations as accurately as possible within the symbolic model.

This tutorial covers Tamarin’s system specification, execution model, and property specification language. I will demonstrate how Tamarin can automatically analyse systems, and how its extensive interactive mode aids in the analysis of more complex systems. Finally, I will touch upon Tamarin’s more advanced features and larger succesful case studies, such as the upcoming TLS 1.3 internet standard.

Jade Alglave, University College London / Microsoft Research

Coalition, intrigue, ambush, destruction and pride: herding cats can be challenging

Abstract: Herding cats can lead to coalition (of cheetahs), intrigue (of kittens), ambush (of tigers), destruction (of wild cats) or pride (of lions). In this tutorial, I will present the cat language to write consistency models as a set of constraints on the executions of concurrent programs. A cat model can be executed within the herd tool, which I will use during the tutorial.

Keynotes

Byron Cook (Senior Principal Engineer, Amazon Web Services and Professor at University College London)

Automated Formal Reasoning About AWS Systems

Abstract: Automatic and semiautomatic formal verification tools are now being developed and used within Amazon Web Services (AWS) to find proofs that prove or disprove desired properties of key AWS components. In this session, we outline these efforts and discuss how tools are used to play and then replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system.

Wilfried Steiner (TTTech)

Formal Methods in Industrial Dependable Systems Design - The TTTech Example

Abstract: Over the last decades the field of dependable computer systems has gained tremendous significance in our modern society. We rely on the dependability of automobiles, railways, airplanes, medical devices, critical infrastructures, like the electrical grid or industrial production facilities, and many more. These dependable systems frequently implement non-trivial mechanisms, for example, to coordinate between redundant components, and a guarantee of correctness of these mechanisms is therefore crucial to avoid catastrophic incidents. Consequently, formal methods are frequently used in industrial dependable system design and in this talk I will discuss the various aspects in which formal methods are and have been deployed for specification, verification, and configuration at TTTech for critical networking products.