The following is a description of the invited talks.
Limin Jia - (Bridging) the gap between formal information flow security analysis and real world applications
The Bell-LaPadula and Biba models developed in the 1970s and the subsequent lattice-based model by Denning were considered cornerstones of computer security and started a long line of research in information flow security. These models described how to protect and use potentially sensitive information and are incredibly useful in formally analyzing security risks of practical systems. When IFTTT, an end-user-programming service that allows users to write if-then-style rules to connect arbitrary IoT devices to each other and to online services, emerged, we applied lattice-based information flow modeling to analyze its security and privacy risks and flagged almost 50% of the rules being dangerous; i.e., violating safe information flow security principles. However, our subsequent user study showed that our formal model is lacking in capturing rich contextual information and as a result, very few of the dangerous information flows flagged by the formal analysis are considered by the users as causing real harm. In this talk, I will discuss where our formal information flow security modeling succeeded and failed to produce useful results and propose directions to help make such formal modeling and analysis practically relevant in protecting users.
Peter Sewell - CHERI capability-enhanced Arm (Morello), RISC-V, and MIPS: semantics, semantics-based testing, and security-property proofs
The root cause of many security vulnerabilities is the lack of protection provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, which provide only coarse-grain virtual-memory-based protection.
CHERI extends conventional architectures with hardware capabilities that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway on the Arm Morello industrial prototype and SoC, shipping in 2022 for academic and industry evaluation, to explore its possible adoption in mass-market commercial processors.
In this talk I'll describe how we've supported CHERI engineering, and increased confidence, with rigorous semantics. We use formal models of the complete instruction-set architectures (ISAs) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice (as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation) and for formal verification. We formalise key intended security properties of the designs, and establish that these hold with mechanised proof. This is for the complete ISA models (complete enough to boot operating systems), without idealisation.
This is joint work mainly by Thomas Bauereiss, Brian Campbell, Thomas Sewell, Kyndylan Nienhuis, Alasdair Armstrong, Prashanth Mundkur, Robert Norton-Wright, and Alexandre Joannou, in collaboration with Arm and the rest of the CHERI team (led by Robert N. M. Watson, Simon W. Moore, Peter Sewell, Peter G. Neumann, and Ian Stark).
Carmela Troncoso - Designing technology in pandemic times
The COVID-19 pandemic has fostered the deployment of new technologies to mitigate the fast expansion of the virus and help society to return to normal. Technology, however, can also cause harm in particular when deployed in a hurry and without adequate safeguards. I this talk I will share my experience in designing, and supporting the deployment of, privacy-preserving technologies to complement manual contact tracing. These technologies are now developed at a large scale.
The following papers have been accepted to CSF 2021. Papers are also available here.