Toby Murray

Verifying that a compiler preserves concurrent value-dependent information-flow security

R Sison, T Murray

Conference Proceedings  |  2019  |  Leibniz International Proceedings in Informatics, LIPIcs

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

Formally Verified Software in the Real World

Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser

Journal article  |  2018  |  Communications of the ACM

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)

© 2018 IEEE. Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive..

BP: Formal Proofs, the Fine Print and Side Effects

T Murray, Paul Van Oorschot

Conference Proceedings  |  2018  |  2018 IEEE Cybersecurity Development (SecDev)

Given recent high-profile successes in formal verification of security-related properties (e.g., for seL4), and the rising popular..

In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces

Abdullah Issa, Toby Murray, Gidon Ernst

Conference Proceedings  |  2018  |  Proceedings of the 30th Australian Conference on Computer-Human Interaction

Short paper: Towards information flow reasoning about real-world C code

S Gruetter, T Murray

Conference Proceedings  |  2017  |  Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security - PLAS '17

Provably trustworthy systems

Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray, Liam O'Connor

Journal article  |  2017  |  Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

Special issue on verified information flow security

Toby Murray, Andrei Sabelfeld, Lujo Bauer

Journal article  |  2017  |  Journal of Computer Security

Permission and authority revisited towards a formalisation

T Murray

Conference Proceedings  |  2016  |  Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs - FTfJP'16

© 2016 ACM. Miller's notions of permissions and authority are foundational to the analysis of object-capability programming. Infor..

A framework for the automatic formal verification of refinement from COGENT to C

C Rizkallah, J Lim, Y Nagashima, T Sewell, Z Chen, L O Connor, T Murray, G Keller, G Klein

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

© Springer International Publishing Switzerland 2016.Our language Cogent simplifies verification of systems software using a certi..

Eisbach: A Proof Method Language for Isabelle

D Matichuk, TC Murray, M Wenzel

Journal article  |  2016  |  Journal of Automated Reasoning

Refinement through restraint: bringing down the cost of verification

L O'Connor, Z Chen, C Rizkallah, S Amani, J Lim, T MURRAY, Y Nagashima, T Sewell, G Klein

Conference Proceedings  |  2016  |  ACM SIGPLAN Notices

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)

The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface

M Beaumont, J McCarthy, T MURRAY

Conference Proceedings  |  2016  |  Proceedings of the 32nd Annual Conference on Computer Security Applications - ACSAC '16

CoGENT: Verifying High-Assurance File System Implementations.

S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, Y Nagashima, J Lim, T Sewell, J Tuong, G Keller, TC Murray, G Klein, G Heiser

Conference Proceedings  |  2016  |  Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS '16

Specifying a realistic file system

S Amani, T Murray

Conference Proceedings  |  2015  |  Electronic Proceedings in Theoretical Computer Science

Short paper: On high-assurance information-flow-secure programming languages

T Murray

Conference Proceedings  |  2015  |  Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security - PLAS'15

Empirical study towards a leading indicator for cost of formal software verification

D Matichuk, T Murray, J Andronick, R Jeffery, G Klein, M Staples

Conference Proceedings  |  2015  |  2015 IEEE/ACM 37th IEEE International Conference on Software Engineering

An empirical research agenda for understanding formal methods productivity

R Jeffery, M Staples, J Andronick, G Klein, T Murray

Journal article  |  2015  |  Information and Software Technology

File systems deserve verification too!

G Keller, T Murray, S Amani, L O'Connor, Z Chen, L Ryzhyk, G Klein, G Heiser

Journal article  |  2014  |  ACM SIGOPS Operating Systems Review

The last mile: An empirical study of timing channels on seL4

D Cock, Q Ge, T Murray, G Heiser

Conference Proceedings  |  2014  |  Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security - CCS '14

An Isabelle proof method language

D Matichuk, M Wenzel, T Murray

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

Comprehensive Formal Verification of an OS Microkernel

G Klein, J Andronick, K Elphinstone, T Murray, T Sewell, R Kolanski, G Heiser

Journal article  |  2014  |  ACM Transactions on Computer Systems

Productivity for proof engineering

M Staples, R Jeffery, J Andronick, T Murray, G Klein, R Kolanski

Conference Proceedings  |  2014  |  Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement - ESEM '14

Formal specifications better than function points for code sizing

M Staples, R Kolanski, G Klein, C Lewis, J Andronick, T Murray, R Jeffery, L Bass

Conference Proceedings  |  2013  |  2013 35th International Conference on Software Engineering (ICSE)

File systems deserve verification too!

G Keller, T Murray, S Amani, L O'Connor, Z Chen, L Ryzhyk, G Klein, G Heiser

Conference Proceedings  |  2013  |  Operating Systems Review (ACM)

On the limits of refinement-testing for model-checking CSP

T Murray

Journal article  |  2013  |  Formal Aspects of Computing

seL4: From general purpose to a proof of information flow enforcement

T Murray, D Matichuk, M Brassil, P Gammie, T Bourke, S Seefried, C Lewis, X Gao, G Klein

Conference Proceedings  |  2013  |  2013 IEEE Symposium on Security and Privacy

Noninterference for operating system kernels

T Murray, D Matichuk, M Brassil, P Gammie, G Klein

Other  |  2012  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Extensible specifications for automatic re-use of specifications and proofs

D Matichuk, T Murray

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

It's time for trustworthy systems

G Heiser, T Murray, G Klein

Journal article  |  2012  |  IEEE Security & Privacy Magazine

Noninterference for Operating System Kernels

TC Murray, D Matichuk, M Brassil, P Gammie, G Klein

Conference Proceedings  |  2012

Provable Security: How Feasible Is It?

G Klein, TC Murray, P Gammie, T Sewell, S Winwood

Conference Proceedings  |  2011

seL4 Enforces Integrity

T Sewell, S Winwood, P Gammie, TC Murray, J Andronick, G Klein

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

Analysing the information flow properties of object-capability patterns

T Murray, G Lowe

Other  |  2010  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Analysing the Security Properties of Object-Capability Patterns

T Murray

Thesis / Dissertation  |  2010

On Refinement-Closed Security Properties and Nondeterministic Compositions

T Murray, G Lowe

Journal article  |  2009  |  Electronic Notes in Theoretical Computer Science

Non-delegatable authorities in capability systems

T Murray, D Grove

Journal article  |  2008  |  Journal of Computer Security

An overview of the annex system

DA Grove, TC Murray, CA Owen, CJ North, JA Jones, MR Beaumont, BD Hopkins

Conference Proceedings  |  2007  |  Twenty-Third Annual Computer Security Applications Conference (ACSAC 2007)

An overview of the annex system

DA Grove, TC Murray, CA Owen, CJ North, JA Jones, MR Beaumont, BD Hopkins

Conference Proceedings  |  2007  |  Twenty-Third Annual Computer Security Applications Conference (ACSAC 2007)