Toby Murray

Deductive verification via the debug adapter protocol

G Ernst, J Blau, T Murray

Journal article  |  2021  |  Electronic Proceedings in Theoretical Computer Science, EPTCS

We propose a conceptual integration of deductive program verification into existing user interfaces for software debugging. This i..

Information-flow control on ARM and POWER multicore processors

Graeme Smith, Nicholas Coughlin, Toby Murray

Journal article  |  2021  |  FORMAL METHODS IN SYSTEM DESIGN

Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can als..

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

Towards Provable Timing-Channel Prevention

G Heiser, T Murray, G Klein

Journal article  |  2020  |  Operating Systems Review (ACM)

We describe our ongoing research that aims to eliminate microarchitectural timing channels through time protection, which eliminat..

VERONICA: Expressive and Precise Concurrent Information Flow Security

D Schoepe, T Murray, A Sabelfeld

Conference Proceedings  |  2020  |  Proceedings - IEEE Computer Security Foundations Symposium

Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the p..

Legion: Best-first concolic testing (competition contribution)

D Liu, G Ernst, T Murray, BIP Rubinstein

Conference Proceedings  |  2020  |  23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Legion is a grey-box coverage-based concolic tool that aims to balance the complementary nature of fuzzing and symbolic execution ..

LEGION: Best-First Concolic Testing

Dongge Liu, Gidon Ernst, Toby Murray, Benjamin IP Rubinstein

Conference Proceedings  |  2020  |  2020 35TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2020)

Concolic execution and fuzzing are two complementary coverage-based testing techniques. How to achieve the best of both remains an..

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

Can We Prove Time Protection?

G Heiser, G Klein, T Murray

Conference Proceedings  |  2019

© 2019 ACM. Timing channels are a significant and growing security threat in computer systems, with no established solution. We ha..

SECCSL: Security concurrent separation logic

G Ernst, T Murray

Conference Proceedings  |  2019  |  Lecture Notes in Computer Science

© The Author(s) 2019. We present SecCSL, a concurrent separation logic for proving expressive, data-dependent information flow sec..