Toby Murray

LEGION: Best-First Concolic Testing

D Liu, G Ernst, T Murray, BIP Rubinstein

Conference Proceedings  |  2020  |  Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Towards Provable Timing-Channel Prevention

G Heiser, T Murray, G Klein

Journal article  |  2020  |  ACM SIGOPS Operating Systems Review

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  |  2020 IEEE 33rd Computer Security Foundations Symposium (CSF)

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  |  Lecture Notes in Artificial Intelligence

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

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  |  Proceedings of the Workshop on Hot Topics in Operating Systems

© 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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

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

Empirically Analyzing Ethereum's Gas Mechanism

Renlord Yang, Toby Murray, Paul Rimba, Udaya Parampalli

Conference Proceedings  |  2019  |  2019 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW)

Ethereum's Gas mechanism attempts to set transaction fees in accordance with the computational cost of transaction execution: a co..

Value-dependent information-flow security on weak memory models

G Smith, N Coughlin, T Murray

Conference Proceedings  |  2019  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

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

Abstract and Concrete Data Types vs Object Capabilities

James Noble, Alex Potanin, T Murray, Mark S Miller

Book Chapter  |  2018

The distinctions between the two forms of procedural data abstraction—abstract data types and objects—are well known. An abstract ..