2019-03-03 Johannes Aman Pohjola has won best paper at FORTE and at the DisCoTeC federated conference

Johannes Aman Pohjola has won best paper at FORTE 2019 and at the DisCoTeC 2019 federated conference. The paper covers the standard theoretical models of concurrent systems with explicit communication channels, such as the pi-calculus, which give rise to symmetric and transitive connectivity between processes. That is, if I can send a message to you, it follows that you can send a message to me, and that I can send a message to anyone you can send to. In this paper, this somewhat unrealistic assumption is relaxed by developing a more general model where channels can denote any connectivity relation, including one-way connections or connections that change over time. Congratulations Johannes!

Tony Hosking wins ARC DP grant on “Verified concurrent memory management on modern processors".
2018-12-03 Tony Hosking wins ARC DP grant on “Verified concurrent memory management on modern processors", which relates to the MicroVM project and CakeML project. Congratulations!

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.