Toby C. Murray

45 papers A* 5A 8B 5Journal 15Unranked 10

Year	Rank	Type	Title / Venue / Authors
2019	A	`conf`	Can We Prove Time Protection? HotOS Gernot Heiser, Gerwin Klein, Toby C. Murray
2019	J	`jnl`	Can We Prove Time Protection? CoRR Gernot Heiser, Gerwin Klein, Toby C. Murray
2019	J	`jnl`	Verifying that a compiler preserves concurrent value-dependent information-flow security. CoRR Robert Sison, Toby C. Murray
2018	—	`conf`	Abstract and Concrete Data Types vs Object Capabilities. Principled Software Development James Noble, Alex Potanin, Toby C. Murray, Mark S. Miller
2018	—	`conf`	BP: Formal Proofs, the Fine Print and Side Effects. SecDev Toby C. Murray, Paul C. van Oorschot
2018	A	`conf`	COVERN: A Logic for Compositional Verification of Information Flow Control. EuroS&P Toby C. Murray, Robert Sison, Kai Engelhardt
2018	J	`jnl`	Formally verified software in the real world. Commun. ACM Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser
2017	—	`conf`	Short Paper: Towards Information Flow Reasoning about Real-World C Code. PLAS@CCS Samuel Grütter, Toby C. Murray
2017	J	`jnl`	Special issue on verified information flow security. J. Comput. Secur. Toby C. Murray, Andrei Sabelfeld, Lujo Bauer
2017	J	`jnl`	VST-Flow: Fine-grained low-level reasoning about real-world C code. CoRR Samuel Grütter, Toby C. Murray
2016	J	`jnl`	A Dependent Security Type System for Concurrent Imperative Programs. Arch. Formal Proofs Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016	B	`conf`	A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
2016	J	`jnl`	COGENT: Certified Compilation for a Functional Systems Language. CoRR Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
2016	A*	`conf`	CoGENT: Verifying High-Assurance File System Implementations. ASPLOS Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C. Murray, Gerwin Klein, Gernot Heiser
2016	J	`jnl`	Compositional Security-Preserving Refinement for Concurrent Imperative Programs. Arch. Formal Proofs Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016	A	`conf`	Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. CSF Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016	J	`jnl`	Eisbach: A Proof Method Language for Isabelle. J. Autom. Reason. Daniel Matichuk, Toby C. Murray, Makarius Wenzel
2016	A*	`conf`	PLAS'16: ACM SIGPLAN 11th Workshop on Programming Languages and Analysis for Security. CCS Toby C. Murray, Deian Stefan
2016	—	`conf`	Permission and Authority Revisited towards a formalisation. FTfJP@ECOOP Sophia Drossopoulou, James Noble, Mark S. Miller, Toby C. Murray
2016	—	`ed.`	Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October 24, 2016 PLAS@CCS Toby C. Murray, Deian Stefan
2016	A	`conf`	Refinement through restraint: bringing down the cost of verification. ICFP Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
2016	A	`conf`	The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface. ACSAC Mark R. Beaumont, Jim McCarthy, Toby C. Murray
2015	J	`jnl`	An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein, Toby C. Murray
2015	—	`conf`	Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein, Mark Staples
2015	—	`conf`	Short Paper: On High-Assurance Information-Flow-Secure Programming Languages. PLAS@ECOOP Toby C. Murray
2015	—	`conf`	Specifying a Realistic File System. MARS Sidney Amani, Toby C. Murray
2014	B	`conf`	An Isabelle Proof Method Language. ITP Daniel Matichuk, Makarius Wenzel, Toby C. Murray
2014	J	`jnl`	Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser
2014	J	`jnl`	File systems deserve verification too! ACM SIGOPS Oper. Syst. Rev. Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
2014	A	`conf`	Productivity for proof engineering. ESEM Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski
2014	A*	`conf`	The Last Mile: An Empirical Study of Timing Channels on seL4. CCS David A. Cock, Qian Ge, Toby C. Murray, Gernot Heiser
2013	—	`conf`	File systems deserve verification too! PLOS@SOSP Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
2013	A*	`conf`	Formal specifications better than function points for code sizing. ICSE Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass
2013	J	`jnl`	On the limits of refinement-testing for model-checking CSP. Formal Aspects Comput. Toby C. Murray
2013	A*	`conf`	seL4: From General Purpose to a Proof of Information Flow Enforcement. IEEE Symposium on Security and Privacy Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein
2012	B	`conf`	Extensible Specifications for Automatic Re-use of Specifications and Proofs. SEFM Daniel Matichuk, Toby C. Murray
2012	J	`jnl`	It's Time for Trustworthy Systems. IEEE Secur. Priv. Gernot Heiser, Toby C. Murray, Gerwin Klein
2012	B	`conf`	Noninterference for Operating System Kernels. CPP Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
2011	A	`conf`	Provable Security: How Feasible Is It? HotOS Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood
2011	B	`conf`	seL4 Enforces Integrity. ITP Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
2010	—	`—`	Analysing the security properties of object-capability patterns. Toby C. Murray
2009	—	`conf`	Analysing the Information Flow Properties of Object-Capability Patterns. Formal Aspects in Security and Trust Toby C. Murray, Gavin Lowe
2008	J	`jnl`	Non-delegatable authorities in capability systems. J. Comput. Secur. Toby C. Murray, Duncan A. Grove
2008	—	`conf`	On Refinement-Closed Security Properties and Nondeterministic Compositions. AVoCS Toby C. Murray, Gavin Lowe
2007	A	`conf`	An Overview of the Annex System. ACSAC Duncan A. Grove, Toby C. Murray, Chris A. Owen, Chris J. North, J. A. Jones, Mark R. Beaumont, Bradley D. Hopkins