The meeting will take place at the Shirley & Spärck Jones Lecture Theatre, The British Computer Society, London.
SCHEDULE OF TALKS
09:00-9:45 Registration with Tea and coffee
9:45-10:00 Welcome
10:00-10:30: Talk: ‘VeTSS: From Old to New’, Philippa Gardner, Imperial College London
10:30-11:00: Talk: Kerstin Eder, University of Bristol
11:00-11:30 Coffee Break
11:30-12:00 Talk: ‘Automatic verification of transparency protocols’, Mark Ryan, University of Birmingham with Vincent Cheval and José Moreira.
Abstract: Transparency protocols are protocols whose actions can be publicly monitored by observers (observers may include regulators, rights advocacy groups, or the general public). The observed actions are typically usages of private keys: decryptions, and signings. Examples of transparency protocols include certificate transparency, cryptocurrency, transparent decryption, and electronic voting. Transparency protocols pose a challenge for automatic verification, because they involve sophisticated data types that have strong properties, such as Merkle trees, which allow compact proofs of data presence and tree extension.
We address this challenge by introducing new features in ProVerif (an automatic tool for verifying security protocols), and a methodology for using them. With our methodology, it is possible to describe the data type quite abstractly, using ProVerif axioms, and prove the correctness of the protocol using those axioms as assumptions. Then, in separate steps, one can define one or more concrete implementations of the data type, and again use ProVerif to show that the implementations satisfy the assumptions that were coded as axioms. This helps make compositional proofs, splitting the proof burden into several manageable pieces.
12:00-12:30 Talk: ‘Security and Legacy at Microsoft’ Matthew Parkinson, Microsoft Research
Abstract: I will cover various approaches Microsoft takes to security particularly memory safety. The talk will cover mitigating existing code, compartmentalising legacy code into new applications, and new safe programming languages at Microsoft. Finally, I will discuss verification and places it could fit into Microsoft.
12:30-14:00 Lunch
14:00-14:30 Talk: ‘Benchmarking and verifying quantum computers’, Petros Wallden, The University of Edinburgh
Abstract: Quantum computation promises to offer great computational speed-ups. In this talk we will first introduce quantum computation dispelling certain misconceptions and presenting the state-of-the-art. Then we will describe briefly each of the five different types of benchmarking and verification that the quantum computing community explores: computation verification, hardware characterisation and testing, component and system benchmarking, software verification, threshold for quantum advantage.
14:30-15:00 Talk: ‘Formal Verification and Bug Finding at Meta’, Jules Villard, Meta
Abstract: While formal verification has been applied with great success in several projects, automating verification techniques to a degree that they can be incorporated in day-to-day software development remains a somewhat distant dream. It is however possible to use formal methods, such as those employed in verification, in environments with large programs and frantic development speeds! Not to prove theorems that such programs have *no* bugs (they do!), but instead to automatically prove that such programs *do* have bugs. In this talk I’ll share some insights gained while turning program verification techniques into bug-finding tools to help programmers at scale.
15:00-15:30 Talk: ‘The Research Institute for Trustworthy Interconnected Cyber-physical Systems’, Chris Hankin, Imperial College London.
Abstract: We will introduce the research programme of RITICS. Highlight some past contributions and identify some areas for possible collaboration between VeTSS and RITICS.
15:30-16:00 Coffee break
16:00-17:00 Short talks session:
‘Design and Verification of Time-Critical Byzantine Fault-Tolerant Systems’, Vincent Rahli, University of Birmingham.
Abstract: The accelerated digitalisation of society along with technological evolution have changed the landscape of cyber-physical systems. Two main threats make the reliable and real-time control of these systems challenging: the uncertainty in the communication infrastructure induced by scale and heterogeneity of the environment and devices; and targeted attacks maliciously worsening the impact of the above-mentioned communication uncertainties, disrupting the correctness of real-time applications. We have recently developed broadcast protocols that tackle these challenges by delivering real-time practical performance, while tolerating arbitrary faults, including malicious attacks. In this talk, we will describe these results and present preliminary work towards formally specifying and verifying such protocols. In particular, this involves formalizing non-traditional “quorum systems” and verifying quantitative timeliness properties as opposed to more traditional qualitative properties safety and liveness properties.
‘CsmithEdge: More Effective Compiler Testing by Handling Undefined Behaviour Less Conservatively’, Karine Even-Mendoza, King’s College London.
Abstract: Compiler fuzzing techniques require a means of generating programs that are free from undefined behaviour (UB) to reliably reveal miscompilation bugs. Existing program generators such as Csmith achieve UB freedom by heavily restricting the form of generated programs. The idiomatic nature of the resulting programs risks limiting the test coverage they can offer and, thus, the compiler bugs they can discover.
In this talk, I will present a new fuzzer, CsmithEdge, which extends Csmith, and via which we investigated the idea of adapting existing fuzzers to be less restrictive concerning UB in the practical setting of C compiler testing. CsmithEdge probabilistically weakens the constraints used to enforce UB freedom thus generated programs are no longer guaranteed to be UB-free. It then employs several off-the-shelf UB detection tools and a novel dynamic analysis to (a) detect UB in generated programs and (b) eliminate UB-freedom constraints for arithmetic operations when Csmith has been too conservative in its use. The resulting UB-free programs are used to test for miscompiled bugs (via differential testing), and the non-UB-free programs are used for crash testing. During our short evaluation, CsmithEdge discovered several previously unknown miscompilation in mature compilers such as GCC, LLVM and MVSC and achieved substantial differences in code coverage on GCC and LLVM compared with regular Csmith.
‘Rust on Morello’, Simon Cooksey, University of Kent.
Abstract: Rust is a language with a rich type system designed to eliminate memory safety bugs in the majority of code, it has seen adoption by major tech companies like Microsoft, Mozilla, and Cloudflare, and is now a second language for the Linux kernel. We explore an approach for porting Rust to the Morello prototype hardware. This has involved changes to the Rust compiler which were interesting and an opportunity to explore some design space. This talk will tell you about the approach we took for porting Rust to Morello, and the bits of friction we encountered on the way. We will also try and give you a taste of where this work is headed next!
17:00-17:30 Panel discussion, with representatives of NCSC, EPSRC, Academy and Industry
17:30-19:00 Drinks Reception