Toby Murray

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

'Free' as in Freedom to Protest?

F Massacci, A Sabetta, J Mirkovic, T Murray, H Okhravi, M Mannan, A Rocha, E Bodden, DE Geer

Journal article  |  2022  |  IEEE Security and Privacy

To kick-start the discussion, let's first review some of the recent attacks. In the node-ipc case1 a developer pushed an update th..

State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing

Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, Benjamin Rubinstein

Conference Proceedings  |  2022  |  2022 29th IEEE International Conference on Software Analysis, Evolution and Reengineering

The statefulness property of network protocol implementations poses a unique challenge for testing and verification techniques, in..

A Hoare Logic with Regular Behavioral Specifications

G Ernst, A Knapp, T Murray

Book Chapter  |  2022  |  Lecture Notes in Computer Science

We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences..

Cogent: uniqueness types and certifying compilation

Liam O'connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller

Journal article  |  2021  |  JOURNAL OF FUNCTIONAL PROGRAMMING

This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating..

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency

Pengbo Yan, Toby Murray

Journal article  |  2021  |  PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL

We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in..

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

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

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

Towards Systematic and Dynamic Task Allocation for Collaborative Parallel Fuzzing

VT Pham, MD Nguyen, QT Ta, T Murray, BIP Rubinstein

Conference Proceedings  |  2021  |  Proceedings - 2021 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021

Parallel coverage-guided greybox fuzzing is the most common setup for vulnerability discovery at scale. However, so far it has rec..