default search action
Toby C. Murray
Toby Murray
Person information
- affiliation: University of Melbourne, School of Computing and Information Systems, Australia
- affiliation: NICTA, Sydney, Australia
- affiliation: University of New South Wales, School of Computer Science and Engineering, Sydney, Australia
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j19]Shing Hing William Cheng, Chitchanok Chuengsatiansup, Daniel Genkin, Dallas McNeil, Toby Murray, Yuval Yarom, Zhiyuan Zhang:
Evict+Spec+Time: Exploiting Out-of-Order Execution to Improve Cache-Timing Attacks. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024(3): 224-248 (2024) - [c48]Mo Zhang
, Eduard Marin
OOBKey: Key Exchange with Implantable Medical Devices Using Out-Of-Band Channels. ARES 2024: 191:1-191:13 - [c47]Pengbo Yan
Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms. FM (1) 2024: 188-205 - [c46]Lianglu Pan
EDEFuzz: A Web API Fuzzer for Excessive Data Exposures. ICSE 2024: 45:1-45:12 - [c45]Vincent Jackson, Toby Murray, Christine Rizkallah:
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. ITP 2024: 23:1-23:16 - [i21]Jiankai Jin, Chitchanok Chuengsatiansup, Toby Murray, Benjamin I. P. Rubinstein
Elephants Do Not Forget: Differential Privacy with State Continuity for Privacy Budget. CoRR abs/2401.17628 (2024) - [i20]Aaron Bembenek, Toby Murray:
Symbol Correctness in Deep Neural Networks Containing Symbolic Layers. CoRR abs/2402.03663 (2024) - [i19]Thanh Le-Cong, Dat Nguyen, Bach Le, Toby Murray:
Evaluating Program Repair with Semantic-Preserving Transformations: A Naturalness Assessment. CoRR abs/2402.11892 (2024) - [i18]Pengbo Yan, Toby Murray, Olga Ohrimenko, Van-Thuan Pham, Robert Sison:
Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version). CoRR abs/2407.00514 (2024) - [i17]Shing Hing William Cheng, Chitchanok Chuengsatiansup, Daniel Genkin, Dallas McNeil, Toby Murray, Yuval Yarom, Zhiyuan Zhang:
Evict+Spec+Time: Exploiting Out-of-Order Execution to Improve Cache-Timing Attacks. IACR Cryptol. ePrint Arch. 2024: 149 (2024) - 2023
- [c44]Toby Murray
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. CCS 2023: 1746-1760 - [c43]Robert Sison
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. FM 2023: 103-121 - [c42]Wentao Gao, Van-Thuan Pham, Dongge Liu
Beyond the Coverage Plateau: A Comprehensive Study of Fuzz Blockers (Registered Report). FUZZING 2023: 47-55 - [c41]Toby Murray, Pengbo Yan, Gidon Ernst
Compositional Vulnerability Detection with Insecurity Separation Logic. ICFEM 2023: 65-82 - [i16]Lianglu Pan, Shaanan Cohney, Toby Murray, Van-Thuan Pham:
Detecting Excessive Data Exposures in Web Server Responses with Metamorphic Fuzzing. CoRR abs/2301.09258 (2023) - [i15]Toby Murray, Mukesh Tiwari, Gidon Ernst
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). CoRR abs/2309.03442 (2023) - [i14]Scott Buckley, Robert Sison
Proving the Absence of Microarchitectural Timing Channels. CoRR abs/2310.17046 (2023) - 2022
- [j18]Fabio Massacci
"Free" as in Freedom to Protest? IEEE Secur. Priv. 20(5): 16-21 (2022) - [c40]Gidon Ernst
A Hoare Logic with Regular Behavioral Specifications. ISoLA (1) 2022: 45-64 - [c39]Dongge Liu
State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. SANER 2022: 720-730 - [i13]Gidon Ernst
A Hoare Logic with Regular Behavioral Specifications. CoRR abs/2205.06584 (2022) - 2021
- [j17]Graeme Smith
Information-flow control on ARM and POWER multicore processors. Formal Methods Syst. Des. 58(1-2): 251-293 (2021) - [j16]Robert Sison
Verified secure compilation for mixed-sensitivity concurrent programs. J. Funct. Program. 31: e18 (2021) - [j15]Liam O'Connor
Cogent: uniqueness types and certifying compilation. J. Funct. Program. 31: e25 (2021) - [j14]Pengbo Yan
SecRSL: security separation logic for C11 release-acquire concurrency. Proc. ACM Program. Lang. 5(OOPSLA): 1-26 (2021) - [c38]Van-Thuan Pham, Manh-Dung Nguyen, Quang-Trung Ta, Toby Murray, Benjamin I. P. Rubinstein
Towards Systematic and Dynamic Task Allocation for Collaborative Parallel Fuzzing. ASE 2021: 1337-1341 - [c37]Gidon Ernst
Deductive Verification via the Debug Adapter Protocol. F-IDE@NFM 2021: 89-96 - [i12]Toby Murray, Pengbo Yan, Gidon Ernst:
Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic. CoRR abs/2107.05225 (2021) - [i11]Pengbo Yan, Toby Murray:
SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices). CoRR abs/2109.03602 (2021) - [i10]Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein:
State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. CoRR abs/2112.15498 (2021) - 2020
- [j13]Toby Murray:
An Under-Approximate Relational Logic. Arch. Formal Proofs 2020 (2020) - [j12]Gernot Heiser, Toby Murray, Gerwin Klein:
Towards Provable Timing-Channel Prevention. ACM SIGOPS Oper. Syst. Rev. 54(1): 1-7 (2020) - [c36]Daniel Schoepe, Toby Murray, Andrei Sabelfeld:
VERONICA: Expressive and Precise Concurrent Information Flow Security. CSF 2020: 79-94 - [c35]Dongge Liu
Legion: Best-First Concolic Testing (Competition Contribution). FASE 2020: 545-549 - [c34]Dongge Liu
LEGION: Best-First Concolic Testing. ASE 2020: 54-65 - [i9]Daniel Schoepe, Toby Murray, Andrei Sabelfeld:
VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices). CoRR abs/2001.11142 (2020) - [i8]Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein:
Legion: Best-First Concolic Testing. CoRR abs/2002.06311 (2020) - [i7]Toby Murray:
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More. CoRR abs/2003.04791 (2020) - [i6]Robert Sison
Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs. CoRR abs/2010.14032 (2020)
2010 – 2019
- 2019
- [c33]Gidon Ernst
SecCSL: Security Concurrent Separation Logic. CAV (2) 2019: 208-230 - [c32]Renlord Yang, Toby Murray, Paul Rimba, Udaya Parampalli:
Empirically Analyzing Ethereum's Gas Mechanism. EuroS&P Workshops 2019: 310-319 - [c31]Graeme Smith
Value-Dependent Information-Flow Security on Weak Memory Models. FM 2019: 539-555 - [c30]Gernot Heiser, Gerwin Klein, Toby C. Murray:
Can We Prove Time Protection? HotOS 2019: 23-29 - [c29]Robert Sison
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. ITP 2019: 27:1-27:19 - [e2]Toby Murray, Gidon Ernst
Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, United Kingdom, July 15, 2019. ACM 2019, ISBN 978-1-4503-6864-3 [contents] - [i5]Gernot Heiser, Gerwin Klein, Toby C. Murray:
Can We Prove Time Protection? CoRR abs/1901.08338 (2019) - [i4]Renlord Yang, Toby Murray, Paul Rimba, Udaya Parampalli:
Empirically Analyzing Ethereum's Gas Mechanism. CoRR abs/1905.00553 (2019) - [i3]Robert Sison
Verifying that a compiler preserves concurrent value-dependent information-flow security. CoRR abs/1907.00713 (2019) - 2018
- [j11]Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser:
Formally verified software in the real world. Commun. ACM 61(10): 68-77 (2018) - [c28]James Noble
Abstract and Concrete Data Types vs Object Capabilities. Principled Software Development 2018: 221-240 - [c27]Toby C. Murray, Robert Sison
COVERN: A Logic for Compositional Verification of Information Flow Control. EuroS&P 2018: 16-30 - [c26]Abdullah Issa, Toby Murray, Gidon Ernst
In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces. OZCHI 2018: 572-576 - [c25]Toby C. Murray, Paul C. van Oorschot:
BP: Formal Proofs, the Fine Print and Side Effects. SecDev 2018: 1-10 - 2017
- [j10]Toby C. Murray, Andrei Sabelfeld, Lujo Bauer:
Special issue on verified information flow security. J. Comput. Secur. 25(4-5): 319-321 (2017) - [c24]Samuel Grütter, Toby C. Murray:
Short Paper: Towards Information Flow Reasoning about Real-World C Code. PLAS@CCS 2017: 43-48 - [i2]Samuel Grütter, Toby C. Murray:
VST-Flow: Fine-grained low-level reasoning about real-world C code. CoRR abs/1709.05243 (2017) - 2016
- [j9]Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah:
A Dependent Security Type System for Concurrent Imperative Programs. Arch. Formal Proofs 2016 (2016) - [j8]Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah:
Compositional Security-Preserving Refinement for Concurrent Imperative Programs. Arch. Formal Proofs 2016 (2016) - [j7]Daniel Matichuk, Toby C. Murray, Makarius Wenzel:
Eisbach: A Proof Method Language for Isabelle. J. Autom. Reason. 56(3): 261-282 (2016) - [c23]Mark R. Beaumont, Jim McCarthy, Toby C. Murray:
The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface. ACSAC 2016: 533-545 - [c22]Sidney Amani, Alex Hixon, Zilin Chen
CoGENT: Verifying High-Assurance File System Implementations. ASPLOS 2016: 175-188 - [c21]Toby C. Murray, Deian Stefan:
PLAS'16: ACM SIGPLAN 11th Workshop on Programming Languages and Analysis for Security. CCS 2016: 1870 - [c20]Toby C. Murray, Robert Sison
Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. CSF 2016: 417-431 - [c19]Sophia Drossopoulou, James Noble, Mark S. Miller, Toby C. Murray:
Permission and Authority Revisited towards a formalisation. FTfJP@ECOOP 2016: 10 - [c18]Liam O'Connor
Refinement through restraint: bringing down the cost of verification. ICFP 2016: 89-102 - [c17]Christine Rizkallah
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP 2016: 323-340 - [e1]Toby C. Murray, Deian Stefan:
Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October 24, 2016. ACM 2016, ISBN 978-1-4503-4574-3 [contents] - [i1]Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein:
COGENT: Certified Compilation for a Functional Systems Language. CoRR abs/1601.05520 (2016) - 2015
- [j6]D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein
An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. 60: 102-112 (2015) - [c16]Toby C. Murray:
Short Paper: On High-Assurance Information-Flow-Secure Programming Languages. PLAS@ECOOP 2015: 43-48 - [c15]Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) 2015: 722-732 - [c14]Sidney Amani, Toby C. Murray:
Specifying a Realistic File System. MARS 2015: 1-9 - 2014
- [j5]Gabriele Keller
File systems deserve verification too! ACM SIGOPS Oper. Syst. Rev. 48(1): 58-64 (2014) - [j4]Gerwin Klein
Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1): 2:1-2:70 (2014) - [c13]David A. Cock
The Last Mile: An Empirical Study of Timing Channels on seL4. CCS 2014: 570-581 - [c12]Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein
Productivity for proof engineering. ESEM 2014: 15:1-15:4 - [c11]Daniel Matichuk, Makarius Wenzel, Toby C. Murray:
An Isabelle Proof Method Language. ITP 2014: 390-405 - 2013
- [j3]Toby C. Murray:
On the limits of refinement-testing for model-checking CSP. Formal Aspects Comput. 25(2): 219-256 (2013) - [c10]Mark Staples, Rafal Kolanski, Gerwin Klein
Formal specifications better than function points for code sizing. ICSE 2013: 1257-1260 - [c9]Gabriele Keller
File systems deserve verification too! PLOS@SOSP 2013: 1:1-1:7 - [c8]Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein
seL4: From General Purpose to a Proof of Information Flow Enforcement. IEEE Symposium on Security and Privacy 2013: 415-429 - 2012
- [j2]Gernot Heiser, Toby C. Murray, Gerwin Klein
It's Time for Trustworthy Systems. IEEE Secur. Priv. 10(2): 67-70 (2012) - [c7]Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
Noninterference for Operating System Kernels. CPP 2012: 126-142 - [c6]Daniel Matichuk, Toby C. Murray:
Extensible Specifications for Automatic Re-use of Specifications and Proofs. SEFM 2012: 333-341 - 2011
- [c5]Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood:
Provable Security: How Feasible Is It? HotOS 2011 - [c4]Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
seL4 Enforces Integrity. ITP 2011: 325-340 - 2010
- [b1]Toby C. Murray:
Analysing the security properties of object-capability patterns. University of Oxford, UK, 2010
2000 – 2009
- 2009
- [c3]Toby C. Murray, Gavin Lowe:
Analysing the Information Flow Properties of Object-Capability Patterns. Formal Aspects in Security and Trust 2009: 81-95 - 2008
- [j1]Toby C. Murray, Duncan A. Grove:
Non-delegatable authorities in capability systems. J. Comput. Secur. 16(6): 743-759 (2008) - [c2]Toby C. Murray, Gavin Lowe:
On Refinement-Closed Security Properties and Nondeterministic Compositions. AVoCS 2008: 49-68 - 2007
- [c1]Duncan A. Grove, Toby C. Murray, Chris A. Owen, Chris J. North, J. A. Jones, Mark R. Beaumont
An Overview of the Annex System. ACSAC 2007: 341-352
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:15 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: