profile icon
Dr

Robert Sison

Research Fellow
Computing and Information Systems
Interactive Theorem Proving
Formal Verification
Formal Methods
Computer Security
Information-Flow Security
computer science
science & technology
technology
secure compilation
Robert Sison's Profile Picture
Dr

Robert Sison

 
Division
Engineering and IT
 
Primary Interest
Formal Verification
Robert Sison's Profile Picture
Dr

Robert Sison

 
Print
Robert's  Short Profile
 

Scholarly Works

Displaying the 6 most recent scholarly works from 6 for Robert Sison.

Scholarly works icon

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems

Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser

Conference Proceedings  |  2023  |  Proceedings of the 25th International Symposium on Formal Methods

Microarchitectural timing channels are a well-known mechanism for information leakage. Time protection has recently been demonstra..

Scholarly works icon

Verified secure compilation for mixed-sensitivity concurrent programs

ROBERT SISON, TOBY MURRAY

Journal article  |  2021  |  Journal of Functional Programming

Proving only over source code that programs do not leak sensitive data leaves a gap between reasoning and reality that can only be..

Scholarly works icon

Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs

Robert Sison

Thesis / Dissertation  |  2020

Here, I pose the thesis that proving noninterference and its preservation by a compiler is feasible for mixed-sensitivity concurre..

Scholarly works icon

Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

R Sison, T Murray

Conference Proceedings  |  2019  |  Proceedings of the 10th International Conference on Interactive Theorem Proving

It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between re..

Scholarly works icon

COVERN: A Logic for Compositional Verification of Information Flow Control

T Murray, R Sison, K Engelhardt

Conference Proceedings  |  2018  |  Proceedings of the 3rd IEEE European Symposium on Security and Privacy

Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive data. Recent..

Scholarly works icon

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference

Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah

Conference Proceedings  |  2016  |  Proceedings of the Computer Security Foundations Workshop

Value-dependent noninterference allows the classification of program variables to depend on the contents of other variables, and t..

6

Scholarly Works

Keyword Analysis

Software Engineering
Information Systems, Technologies and Services
Cybersecurity and Privacy
Distributed Computing and Systems Software
Expanding Knowledge

Honours, Awards and Fellowships

2021

Eureka Prize for Outstanding Science in Safeguarding Australia (Cross Domain Desktop Compositor team)

Australian Museum
2018

Attendance at Summer School Marktoberdorf (Engineering Secure and Dependable Software Systems)

fortiss GmbH
2018

Travel support to attend DeepSpec Summer School on Verified Systems (DSSS'18)

Princeton University
2017

Travel support to attend Programming Languages Mentoring Workshop (PLMW@POPL'18)

ACM SIGPLAN
2016

CSIRO Data61 Research Project Award (PhD top-up scholarship)

CSIRO's Data61

5

Awards

Credentials

Positions

Research Fellow

Computing and Information Systems

Education

Doctor of Philosophy (Computer Science and Engineering)

University of New South Wales

Master of Information Technology with Excellence

University of New South Wales

Bachelor of Engineering (Computer Engineering) with Honours Class 1, and Bachelor of Arts (Japanese Studies), combined

University of New South Wales

Links