Robert Sison

Robert is a Research Fellow for the School of Computing and Information Systems who 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 information-flow security, also known as confidentiality.

Robert began his career as a software engineer for Open Kernel Labs, Inc. and General Dynamics C4 Systems, where he developed device-driver paravirtualisation stacks for use by Android and Linux kernel instances on a dual-personality smartphone. Subsequently, as a research engineer for NICTA and CSIRO's Data61 during his master's studies, Robert ported the eChronos real-time operating system to the PowerPC e500, and assisted research on formal methods for proving and preserving concurrent value-dependent notions of noninterference, the strictest kind of confidentiality property. His doctoral thesis, currently under examination, concerns the practical application of those methods to the verification of both (1) concurrent programs that might reuse shared memory to hold data of different sensitivity levels at different times, and (2) their compilers, respectively to enforce and to preserve such noninterference properties. He holds a Master of Information Technology with Excellence, awarded in August 2016; and a Bachelor of Engineering in Computer Engineering with Honours Class 1, awarded in May 2010, both from the University of New South Wales.