Robert Sison

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..

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..

COVERN: A Logic for Compositional Verification of Information Flow Control

T Murray, R Sison, K Engelhardt

Conference Proceedings  |  2018  |  2018 IEEE European Symposium on Security and Privacy (EuroS&P)

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

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference

Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah

Conference Proceedings  |  2016  |  2016 IEEE 29th Computer Security Foundations Symposium (CSF)