Congratulations to Dr Qian Ge!

2019-10-04 Congratualtions to Dr Qian Ge, who has just been awarded her PhD! Qian had been working on inventing highly optimised OS mechanisms for mitigating microarchitectural timing channels which obtain data leakage through resource contention. Her and her co-authors proposed a new system concept, time protection, as an OS abstraction, which offers mandatory temporal isolation analogous to the spatial isolation provided by the established memory protection abstraction. Time protection provides security guarantees against microarchitectural timing channels through a combination of temporal and spatial isolation techniques. Using our prototype in the seL4 microkernel, they demonstrated that time protection is both lightweight and effective.

Congratulations to Dr Liam O'Conner!
2019-09-26 Congratulations to Liam O'Conner, who has just been awarded his PhD! Liam has been instrumental in the design of the Cogent language, a functional systems language that can be reasoned about, while producing fast C code. A major part of his thesis was formalising the refinement from a functional semantics to an imperative semantics of Cogent by using linear types.

June Andronick is an invited speaker to FM'19
2019-06-06 FM '19 is the third world congress on Formal Methods (held every 10 years). It's is in Porto this October, where our research group leader June Andronick is an invited speaker! You can learn more about FM'19 from this video.

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!