Toby C. Murray

Orcid: 0000-0002-8271-0289

Affiliations:
  • University of Melbourne, School of Computing and Information Systems, Australia
  • NICTA, Sydney, Australia
  • University of New South Wales, School of Computer Science and Engineering, Sydney, Australia


According to our database1, Toby C. Murray authored at least 81 papers between 2007 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Evict+Spec+Time: Exploiting Out-of-Order Execution to Improve Cache-Timing Attacks.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024

Semantic-guided Search for Efficient Program Repair with Large Language Models.
CoRR, 2024

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version).
CoRR, 2024

Evaluating Program Repair with Semantic-Preserving Transformations: A Naturalness Assessment.
CoRR, 2024

Symbol Correctness in Deep Neural Networks Containing Symbolic Layers.
CoRR, 2024

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras.
Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

EDEFuzz: A Web API Fuzzer for Excessive Data Exposures.
Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, 2024

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms.
Proceedings of the Formal Methods - 26th International Symposium, 2024

Elephants Do Not Forget: Differential Privacy with State Continuity for Privacy Budget.
Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024

OOBKey: Key Exchange with Implantable Medical Devices Using Out-Of-Band Channels.
Proceedings of the 19th International Conference on Availability, Reliability and Security, 2024

2023
Proving the Absence of Microarchitectural Timing Channels.
CoRR, 2023

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version).
CoRR, 2023

Detecting Excessive Data Exposures in Web Server Responses with Metamorphic Fuzzing.
CoRR, 2023

Compositional Vulnerability Detection with Insecurity Separation Logic.
Proceedings of the Formal Methods and Software Engineering, 2023

Beyond the Coverage Plateau: A Comprehensive Study of Fuzz Blockers (Registered Report).
Proceedings of the 2nd International Fuzzing Workshop, 2023

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems.
Proceedings of the Formal Methods - 25th International Symposium, 2023

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications.
Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022
"Free" as in Freedom to Protest?
IEEE Secur. Priv., 2022

State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing.
Proceedings of the IEEE International Conference on Software Analysis, 2022

A Hoare Logic with Regular Behavioral Specifications.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

2021
SecRSL: security separation logic for C11 release-acquire concurrency.
Proc. ACM Program. Lang., 2021

Verified secure compilation for mixed-sensitivity concurrent programs.
J. Funct. Program., 2021

Cogent: uniqueness types and certifying compilation.
J. Funct. Program., 2021

Information-flow control on ARM and POWER multicore processors.
Formal Methods Syst. Des., 2021

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices).
CoRR, 2021

Deductive Verification via the Debug Adapter Protocol.
Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic.
CoRR, 2021

Towards Systematic and Dynamic Task Allocation for Collaborative Parallel Fuzzing.
Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering, 2021

2020
Towards Provable Timing-Channel Prevention.
ACM SIGOPS Oper. Syst. Rev., 2020

An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More.
CoRR, 2020

VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices).
CoRR, 2020

An Under-Approximate Relational Logic.
Arch. Formal Proofs, 2020

LEGION: Best-First Concolic Testing.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Legion: Best-First Concolic Testing (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2020

VERONICA: Expressive and Precise Concurrent Information Flow Security.
Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

2019
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Can We Prove Time Protection?
Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

Value-Dependent Information-Flow Security on Weak Memory Models.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Empirically Analyzing Ethereum's Gas Mechanism.
Proceedings of the 2019 IEEE European Symposium on Security and Privacy Workshops, 2019

SecCSL: Security Concurrent Separation Logic.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Formally verified software in the real world.
Commun. ACM, 2018

BP: Formal Proofs, the Fine Print and Side Effects.
Proceedings of the 2018 IEEE Cybersecurity Development, SecDev 2018, Cambridge, MA, USA, 2018

In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces.
Proceedings of the 30th Australian Conference on Computer-Human Interaction, 2018

COVERN: A Logic for Compositional Verification of Information Flow Control.
Proceedings of the 2018 IEEE European Symposium on Security and Privacy, 2018

Abstract and Concrete Data Types vs Object Capabilities.
Proceedings of the Principled Software Development, 2018

2017
Special issue on verified information flow security.
J. Comput. Secur., 2017

VST-Flow: Fine-grained low-level reasoning about real-world C code.
CoRR, 2017

Short Paper: Towards Information Flow Reasoning about Real-World C Code.
Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, 2017

2016
Eisbach: A Proof Method Language for Isabelle.
J. Autom. Reason., 2016

COGENT: Certified Compilation for a Functional Systems Language.
CoRR, 2016

Compositional Security-Preserving Refinement for Concurrent Imperative Programs.
Arch. Formal Proofs, 2016

A Dependent Security Type System for Concurrent Imperative Programs.
Arch. Formal Proofs, 2016

A Framework for the Automatic Formal Verification of Refinement from Cogent to C.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Refinement through restraint: bringing down the cost of verification.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Permission and Authority Revisited towards a formalisation.
Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, 2016

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

PLAS'16: ACM SIGPLAN 11th Workshop on Programming Languages and Analysis for Security.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

CoGENT: Verifying High-Assurance File System Implementations.
Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface.
Proceedings of the 32nd Annual Conference on Computer Security Applications, 2016

2015
An empirical research agenda for understanding formal methods productivity.
Inf. Softw. Technol., 2015

Specifying a Realistic File System.
Proceedings of the Proceedings Workshop on Models for Formal Analysis of Real Systems, 2015

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Short Paper: On High-Assurance Information-Flow-Secure Programming Languages.
Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, 2015

2014
Comprehensive formal verification of an OS microkernel.
ACM Trans. Comput. Syst., 2014

File systems deserve verification too!
ACM SIGOPS Oper. Syst. Rev., 2014

An Isabelle Proof Method Language.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Productivity for proof engineering.
Proceedings of the 2014 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, 2014

The Last Mile: An Empirical Study of Timing Channels on seL4.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013
On the limits of refinement-testing for model-checking CSP.
Formal Aspects Comput., 2013

seL4: From General Purpose to a Proof of Information Flow Enforcement.
Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Formal specifications better than function points for code sizing.
Proceedings of the 35th International Conference on Software Engineering, 2013

2012
It's Time for Trustworthy Systems.
IEEE Secur. Priv., 2012

Extensible Specifications for Automatic Re-use of Specifications and Proofs.
Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Noninterference for Operating System Kernels.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
seL4 Enforces Integrity.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Provable Security: How Feasible Is It?
Proceedings of the 13th Workshop on Hot Topics in Operating Systems, 2011

2010
Analysing the security properties of object-capability patterns.
PhD thesis, 2010

2009
Analysing the Information Flow Properties of Object-Capability Patterns.
Proceedings of the Formal Aspects in Security and Trust, 6th International Workshop, 2009

2008
Non-delegatable authorities in capability systems.
J. Comput. Secur., 2008

On Refinement-Closed Security Properties and Nondeterministic Compositions.
Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems, 2008

2007
An Overview of the Annex System.
Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC 2007), 2007


  Loading...