Thomas Sewell is a 2019 CORE Award Winner!

2019-05-06 CORE (Computing Research & Education) have awarded Thomas Sewell the John Makepeace Bennett Award for the Australasian Distinguished Doctoral Dissertation! Thomas' PhD on binary translation validation is a breakthrough in formal verification: it manages to prove that the binary code emitted by a standard gcc compiler correctly implements the semantics of the input C program. His tool chain produces a separate proof for each input program -- when gcc produces correct output, the tool confirms with a proof, and when gcc produces incorrect output, it rejects. This is highly significant, as it means that the compiler no longer has to be trusted, and an off-the-shelf low-assurance compiler can be used to produce high-assurance code. The tool chain and methods developed in Thomas' PhD have further applications beyond binary verification. In particular, it enables making an analysis for worst-case execution time (WCET) to be more precise and highly assured.

Yuval Yarom and co-authors win Distinguished Paper Award at 40th IEEE Symposium on Security and Privacy
2019-05-03 The Distinguished Paper Award at 40th IEEE Symposium on Security and Privacy has been awarded to the "Spectre Attacks: Exploiting Speculative Execution" paper, which features Trustworthy Systems' own Yuval Yarom as a co-author. Congratulations!

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.