Professor Gernot Heiser, Dr Toby Murray, and Professor Gerwin Klein have won an ARC discovery grant for their work on provable time protection

2018-11-18 Professor Gernot Heiser, Dr Toby Murray, and Professor Gerwin Klein have won an ARC discovery grant for their work on provable time protection. This project aims to develop techniques to solve the issue in information security of unauthorised information flow resulting from competition for shared hardware resources. The project will combine operating systems design, formal hardware models, information-flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. The project is expected to result in a system that prevents leakage of critical information, such as encryption keys, through timing channels. This should prevent sophisticated attacks on public clouds, mobile devices and military-grade cross-domain devices.

First Annual seL4 Summit

2018-11-05 Supported by Defense Advanced Research Projects Agency (DARPA) and Air Force Research Laboratory (AFRL), the first Annual seL4 Summit will be held on November 14-16, 2018 at the Hilton Washington Dulles Airport, Herndon, VA. seL4 is the first formally verified microkernel, which offers fundamental software separation properties and provides new opportunities to build assured computer systems. The seL4 Summit is part of an effort to establish a Center of Excellence for seL4 ecosystems, aiming to mature the seL4 technology, stabilize the software distribution, train and expand the user base, and develop needed capabilities. The development of seL4 was supported by the Defense Advanced Research Projects Agency (DARPA) under the High-Assurance Cyber Military Systems (HACMS) program, which aims to create technology for the construction of high-assurance cyber-physical systems, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties. Information about Summit agenda, venue and registration can be found at https://www.sel4-us.org/summit.

Qian Ge and co-authors win Best Paper award at APSys 2018

2018-10-03 The paper “No security without time protection: we need a new hardware-software contract” by Qian Ge, Yuval Yarom and Gernot Heiser won Best Paper at the APSys Workshop in Korea. It demonstrates that contemporary processors lack the mechanisms that the operating system (OS) needs to prevent timing channels of the kind that enable the Spectre attacks. The paper consequently proposes an improved hardware-software contract that gives the OS the means to prevent such channels.

An international team including Yuval Yarom revealed Foreshadow at the 2018 Usenix Security Conference
2018-08-16 Following on from Spectre and Meltdown, an international team including Yuval Yarom discovered that using speculative execution on recent Intel processors can be used to extract information that is meant to be hidden by Intel Software Guard eXtensions (SGX). Intel have since extended the scope of the attack: you can read more here.

seL4 now runs on RISC-V64
2018-04-18 Release 9.0.1 of the seL4 kernel has prototype support for RISC-V64. At the time of release, seL4-test passes on the Spike emulation platform, with single core, and without FPU. Full details were released to the seL4 devel mailing list