Robert Sison
Research Scientist; Research Fellow, University of Melbourne
Research Interests
Robert is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale. His current research concerns the formal verification of operating systems to enforce increasingly useful forms of information-flow security, also known as confidentiality.
Contact Details
| Email: | Robert.Sison@data61.csiro.au |
|---|---|
| Web: | https:/ |
More contact information is available at the Contact page.
Robert is a visiting scientist who contributes to the Time Protection verification project.
Robert's PhD with Trustworthy Systems and UNSW Sydney was 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.
Projects
Current |
Past |
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 paravirtualisation stacks for use by Android and Linux kernel instances on a dual-personality smartphone.
Qualifications
Robert holds a Doctor of Philosophy (Computer Science and Engineering), a Master of Information Technology with Excellence, and a Bachelor of Engineering (Computer Engineering) with First Class Honours, all from the University of New South Wales.
Affiliations
Robert holds the position of Research Fellow in Verified Operating System Security with the School of Computing and Information Systems at the University of Melbourne.
Publications
Data61 Papers
2019
 
|
 |
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 |
2018
|
|
|
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 |
|
|
|
Robert Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018 |
NICTA Papers
2016
|
|
|
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 |