Skip to main content

Robert Sison
PhD Student; UNSW Sydney

Research Interests

Robert is broadly interested in discovering how one may design and construct software systems with formally proved information-flow security properties at scale. The research focus of his PhD is to determine the requirements for verifying formally that a compiler doesn't break the information-flow security properties of the programs it's compiling – even when those programs use concurrency, and reuse system resources to process information of differing classification levels at different times.

Contact Details

More contact information is available at the Contact page.

Photo of Robert Sison

Publication List

Robert is a PhD student supervised by Carroll Morgan, Toby Murray, and Kai Engelhardt.

For his machine-checked Isabelle/HOL formalisation of a compiler and proof that it preserves concurrent value-dependent noninterference, please see the COVERN project.




Career Summary

Previously at NICTA and Data61, Robert was a research engineer developing software for the eChronos/SMACCM project, during which time he ported eChronos to the PowerPC e500. Subsequently as a research engineer he developed proofs for the Information Flow project.

Prior to that, he was a software engineer at Open Kernel Labs, Inc. and General Dynamics C4 Systems, where he spent most of his time developing device driver (para)virtualisation stacks for use by Android and Linux kernel instances on a dual-personality smartphone.


Robert holds a Master of Information Technology with Excellence, and a Bachelor of Engineering (Computer Engineering) with First Class Honours, both from the University of New South Wales.


Data61 Papers


PDF Robert Sison and Toby Murray
Verifying that a compiler preserves concurrent value-dependent information-flow security
International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019


Abstract PDF Toby Murray, Robert Sison and Kai Engelhardt
COVERN: A logic for compositional verification of information flow control
European Conference on Security and Privacy (EuroS&P), London, United Kingdom, April, 2018
PDF Robert Sison
Per-thread compositional compilation for confidentiality-preserving concurrent programs
2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018

NICTA Papers


Abstract PDF Toby Murray, Robert Sison, Ed Pierzchalski and Christine Rizkallah
Compositional verification and refinement of concurrent value-dependent noninterference
IEEE Computer Security Foundations Symposium, pp. 417–431, Lisbon, Portugal, June, 2016

Served by Apache on Linux on seL4.