I'm humbled to announce that our entry (with Mark Beaumont of DST Group, and my ex-PhD student and now postdoc Robert Sison) was awarded the 2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia. Our entry describes the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 ] and the formal methods we developed to analyse the security of its concurrent software design [IEEE European Symposium on Security & Privacy (EuroS&P) 2018 ]. Many others have contributed to the CDDC project since its original conception at DST Group, not least Kevin Elphinstone who co-led the CDDC collaboration with me at NICTA, and this recognition attests to the long-term team effort that continues to underpin the success of this project.
I'm delighted to announce that my PhD student Pengbo Yan and I have a paper that will be appearing at OOPSLA 2021. Our paper describes SecRSL which is a program logic we developed for proving that concurrent C programs that make use of C11's Release-Acquire weak memory features are information-flow secure. SecRSL is the first information flow logic developed for a high-level language able to reason about weak-memory concurrency. Moreover it is the first security separation logic proved sound over an axiomatic memory model, and so our paper also presents the first formal definition of information flow security for an axiomatic memory model. We describe not only SecRSL but also how we applied it to verify a range of secure concurrency primitives and how, by taking advantage of C11's weak-memory concurrency features, those primitives perform much better than their traditional sequentially-consistent counterparts. We hope SecRSL will herald many more secure concurrent programs in future.
SecRSL is the latest success from my ongoing COVERN project.
I'm humbled to announce that our entry (with Mark Beaumont of DST Group, and my ex-PhD student and now postdoc Robert Sison) has been selected as a finalist for the 2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia. Our entry describes the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 ] and the formal methods we developed to analyse the security of its concurrent software design [IEEE European Symposium on Security & Privacy (EuroS&P) 2018 ]. Many others have contributed to the CDDC project since its original conception at DST Group, not least Kevin Elphinstone who co-led the CDDC collaboration with me at NICTA, and this recognition attests to the long-term team effort that continues to underpin the success of this project.
We have a wonderful program organised for the 7th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2021), which I'm delighted to be chairing. HotSpot is co-located with IEEE EuroS\&P 2021 and will be held online.
Our program includes talk from leading researchers working on security foundations, attacks and defenses. Registration is just 60 EUR and includes access to all EuroS\&P events. I hope to see you there!
User interfaces in so-called auto-active program verifiers like SPARK Prover, Dafny, and VeriFast have evolved little over the past decade. When a program fails to verify, the user is given very little information about why a proof has failed. Yet detailed information is critical to verify programs productively.
In a recent paper, to be published at F-IDE 2021, we explain and demonstrate how we can use the traditional user interface provided by interactive program debuggers to help debug proof failures. We prototyped this approach for our own SecC program verifier, using the Debug Adapter Protocol integrated into Visual Studio Code.
I am delighted to share that Than Nguyen's MPhil thesis corrections were officially approved today. Than's thesis formalised in Isabelle/HOL a theory of Holistic Specifications of Sophia Drossopoulou and collaborators, including proving key lemmas for their use in reasoning about programs that must interact with and operate in adversarial environments. Than's thesis was supervised with my wonderful colleage and collaborator Ben Rubinstein.
I'm very proud to share that my PhD student Dongge Liu, supervised with Ben Rubinstein and Gidon Ernst, publishsed his first paper, on his automated test-generation tool Legion, at ASE 2020. Legion proposes a principled combination of concolic testing and fuzzing, generalising both, treating automated test generation as an instance of AI search.
Legion proposes Approximate Path Preserving Fuzzing (APPFuzzing), an extension of constrained sampling, to generaise both concolic execution and mutation fuzzing. To decide what program paths to (symbolically) explore, Legion leverages feedback from APPFuzzing: specifically, it casts program exploration as in instance of Monte-Carlo Tree Search (MCTS), using a reward function that favours those parts of the program in which APPFuzzing has found more unique paths in the past. MCTS is known to be an effective way to prioritise search through large spaces, e.g. famously applied by AlphaGo. You can read more about Legion and our approach in the ASE paper, openly available here: https://arxiv.org/abs/2002.06311. Our code is also open source, on GitHub: https://github.com/Alan32Liu/Legion.
I am pleased to announce that Robert Sison, who just submitted his PhD thesis at UNSW, has joined as a postdoc, to work on the Time Protection project, a collaboration with Data61 and UNSW to prove that the seL4 kernel can defend against timing channels. Rob brings with him a wealth of experience in verified information flow security. During his PhD he developed the COVERN Compiler, which was the first verified compiler proved to preserve information flow security for concurrent programs, besides other achievements.
Many secure systems intentionally leak information. Proving them secure therefore means proving that they leak only the information they should leak, and only at the right times. Proving so-called secure declassification policies is a known challenging task and until very recently we have had no satisfactory methods for doing so for concurrent programs. I am therefore pleased to announce, in collaboration with Andrei Sabelfeld and Daniel Schoepe of Chalmers University of Technology, the open source release of VERONICA, which embodies a new formal approach for proving such policies for concurrent programs. VERONICA achieves a radical increase in precision and expressiveness over previous approaches, by utilising a new technique we developed called Decoupled Functional Correctness and is implemented and proved sound from first principles in the Isabelle theorem prover.
You can learn more about VERONICA in our paper recently published at the 2020 IEEE Computer Security Foundations Symposium (CSF).
This work is part of the ongoing COVERN project that I lead, which focuses on methods for proving the security of concurrent programs.
My excellent PhD student Dongge Liu has been developing a new tool called Legion, for automatically generating test cases for programs, that generalises traditional concolic testing and fuzzing. Legion orchestrates program exploration via Monte-Carlo Tree Search. Legion recently took place in the 2nd Competition on Software Testing (Test-Comp 2020), which is a fantastic achievement for Dongge and his efforts over the past year of his PhD. Further details about Legion are forthcoming in a future paper. However, in the meantime you can get a sneak peek by reading our competition contribution short paper, which appeared at FASE 2020.
Much of my recent research has focused on how to prove that programs don't leak sensitive information, using logic. But can we use logic to do the reverse? That is, prove that a program does leak information?
The answer is yes! I have just published to the Archive of Formal Proofs the first Under-Apporoximate Relational Program Logic. Amongst other things, this logic is capable of proving when programs are insecure. It has been fully mechanised in the Isabelle/HOL proof assistant, where it is proved both sound and complete. This development also shows how the traditional notion of relational decomposition applies in the context of under-approximate logics. It builds on recent ideas on program logics for detecting bugs.
I'm very pleased to announce that Mukesh Tiwari has joined us as a postdoc, to continue our work on Security Concurrent Separation Logic (SecCSL), for formally reasoning about information flow for concurrent programs. Mukesh joins us after a PhD at ANU, where he researched how to apply formal methods to make electronic voting more secure.
Timing channels plague modern systems, undermining their security. Yet no operating system provides provable protection against them. We believe that seL4 can be the first kernel to meet this challenge, building on its world-first proof of confidentiality enforcement and its unique mechanisms for implementing time protection.
I'm seeking a postdoc researcher to work with me, Gerwin Klein, Gernot Heiser, and the seL4 team, to make this vision a reality. Further details about the project and the approach we are taking can be found in our position paper, which appeared at HotOS 2019.
To apply, or fore more information, visit: http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security. Applications close: February 25, 09:00am Australian Eastern Daylight Time (GMT +11).
Congratulations to my outstanding PhD student Rob Sison who just presented his first first-author paper at the International Conference on Interactive Theorem Proving (ITP) 2019. The paper presents the verification of the COVERN Compiler, a proof of concept compiler from a simple While language to a simple RISC assembly language that, unlike every other compiler on earth, supports compilation of shared-memory concurrent programs while provably preserving information flow security. The compiler artifact is freely available and its verification rests on a new technique for decomposing proofs of concurrent value-dependent noninterference into a set of simpler proof obligations (see the paper for further details).
This work is part of the COVERN project, which is investigating methods for proving that concurrent programs do not leak sensitive information.
Gidon Ernst and I are thrilled to announce the initial release of the SecC automatic program verifier. SecC is the first program verifier to support automatically proving expressive information flow security for concurrent programs. SecC supports a (growing) subset of the C programming language. Its code is open source and we are using it as the foundation for a number of ongoing research activities.
SecC is powered by a new program logic for concurrent information flow security: security concurrent separation logic. Check out our CAV 2019 paper for the technical details.
Congratulations to Renlord Yang, my indomitable PhD student who just published his first paper at the 2019 IEEE Workshop on Security & Privacy on the Blockchain (IEEE S&B). The paper is the first detailed empirical analysis of this critical mechanism that underpins the security of Ethereum's blockchain, given its Turing-complete smart contract language. Renlord's analysis reveals a number of surprises (including potential denial-of-service attack vectors and gas mispricings) and sets a benchmark for future empirical performance analyses of blockchain platforms.
I am currently advertising a two-year position for a researcher (either a graduate with suitable experience or a postdoc) to research methods for verifying information flow security for shared-memory concurrent programs executing on weak memory consistency models. Further details are here. Applications close: April 30, 11:55pm Australian Eastern Standard Time (GMT +10).
Gidon Ernst and I are co-chairing the 21st Workshop on Formal Techniques for Java-like Programs (FTFJP 2019. The Call for Papers is live and submissions close Sunday, 21st April 2019, (AoE). Please consider submitting!
My team's first foray into the world of usable security will appear at OzCHI 2018, Australia's leading Human Computer Interaction (HCI) research venue. As part of our ongoing work around the Cross Domain Desktop Compositor [Annual Computer Security Applications Conference (ACSAC) 2016 ], we carried out a small user study to investigate the validity of one of the basic assumptions that underpins such systems: that users will behave securely, once sufficiently trained and motivated to protect sensitive information. Our initial results (our aggregate, anonymous data are available online) were encouraging, and highlight the need for this kind of empirical usable security evaluation to complement more traditional means of assurance. However we have barely scratched the surface and there remains much more work to be done in this area.
Credit and thanks goes to my student Abdullah Issa, who performed this research as part of his Masters of Computer Science degree.
Best Paper Award at SecDev 2018
I'm delighted to report that our recent paper “Formal Proofs, the Fine Print and Side Effects” was chosen as the inaugural Best BP Paper at the IEEE Cybersecurity Development Conference (SecDev) 2018.
BP here stands for “Best Practices”, a new category of papers added to the SecDev 2018 call for papers to solicit work that provides an “in-depth clarification and integration of solutions on a major security area.” Our paper focused on the role of formal proofs for building secure systems. You can read more about it in the high level blog post I wrote to mark the award.
Congratulations to Daniel Matichuk, whose PhD thesis Automation for Proof Engineering: Machine-Checked Proofs At Scale recently passed examination at UNSW! Daniel's thesis explores the use of automation for tackling the scalability challenges in large-scale proof engineering efforts, in the context of the Isabelle proof assistant. I'm honoured to have co-supervised Daniel's PhD alongside Gerwin Klein at Data61 and UNSW.
Continuing its success at the 2017 iAwards, the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 ] was this week recognised at the Canberra OpenGov Leadership Forum 2018 for “innovative and disruptive use of technology in the public sector”, via OpenGov's Recognition of Excellence Award. The CDDC is a joint collaboration between Data61 and DST Group that Kevin Elphinstone and I, in our Data61 capacities, established with Mark Beaumont and Chris North of DST Group. Data61 and DST Group were each awarded OpenGov's Recognition of Excellence award.
Paul van Oorschot and I have just made available a draft of an upcoming paper, “Formal Proofs, the Fine Print and Side Effects” [to appear at IEEE Secure Development Conference (SecDev) 2018 ], which takes a critical look at the role of formal proofs for developing secure software.
This paper is aimed primarily at those who want to better understand what value and drawbacks proofs have for secure software development. Formal verification is currently receiving a lot of attention. We believe that it is important, especially for those outside the verification community, to understand its value as well as its shortcomings. Rather than seed doubt on the enterprise of proof and formal verification, our aim is to stimulate interest and further exploration. To quote from the anonymous reviewers:
“The paper provides a very readable introduction to the topic, clarifying the differing interpretations of "the meaning of proofs", and resulting misunderstandings. The presentation is elaborated with many examples from recent literature and state of the art verification efforts. The paper raises a number of important unanswered questions on the relationship between formal methods and security assessments of real systems.”
We hope that this paper will seed ongoing efforts to better understand how proofs can be used most effectively to build secure systems.
I am very excited to welcome Dr Gidon Ernst, who has joined the School of Computing and Information Systems as a postdoctoral Research Fellow. Gidon is working with me on the COVERN project and brings deep expertise on systems program verification and reasoning about heap-manipulating programs, amongst many other things.
The COVERN project (Compositional Verification and Refinement of Noninterference) has gone open source! This project is a major part of my group's ongoing work on verified Information Flow Security for concurrent programs. The COVERN project has developed two major artifacts (both of which are under active development):
At the heart of COVERN is its support for data-dependent classification, in which the sensitivity of data can be dictated by other data. The COVERN logic exploits this to allow natural specifications of information flow contracts between concurrently-executing components, to support compositional reasoning. The COVERN compiler is the first one we know of that is verified to preserve data-dependent noninterference for concurrent programs.
The COVERN logic is described in our research paper [IEEE European Symposium on Security & Privacy (EuroS&P) 2018 ]. That paper also discusses how we applied the COVERN logic to model and verify the functionality of the software components of our award-winning Cross Domain Desktop Compositor (CDDC) system, and to our knowledge is the first foundational machine-checked proof of information flow security for a non-trivial shared-memory concurrent program in the literature.
Congratulations to Yude Lin, whose PhD thesis Symbolic Execution with Over-Approximation today passed examination! Yude's thesis explores how to solve the scalability problems of symbolic execution by over-approximating potential program behaviour. I'm honoured to have played a role after joining Yude's supervision team in 2016 as a co-supervisor, alongside my colleagues Tim Miller and Harald Sondergaard with whom Yude began his PhD journey.
I was recently invited to speak to the Faculty of IT PhD students at Monash University on the topic of Overcoming Adversity in Graduate Research. I took the opportunity to talk about my experiences as a D.Phil. student, and those of other PhD students I have known or supervised, drawing on common experiences and debunking common misconceptions along the way. Thank you to everyone who attended and kudos to the Graduate Research Students Committee (pictured) for organising such a wonderful event and for giving this topic the attention it deserves.
The PhD journey is one of the hardest that many of us will have had to make by that stage in our lives. It is uniquely demanding not least because of the intellectual challenges it presents. Given that so many of us face so many common challenges during that journey, we should be spending much more time talking about them. This talk was one way for me to do that publicly, for which I'm grateful.
You can read a summary of the talk in the following blog post.
Following on from our earlier success at the state level, the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 ] last night won not one but two of the national iAwards. The CDDC was named the national:
The CDDC is a joint collaboration between Data61 and DST Group that Kevin Elphinstone and I, in our Data61 capacities, established with Mark Beaumont (pictured, left) and Chris North (second from left) of DST Group's Active Security Technologies Group, in 2014. Daniella Traino (right) has been instrumental in pursuing commercialisation pathways for the CDDC (as was Jodi Steel before her), along with senior leadership in Data61's Trustworthy Systems Group including Gernot Heiser (second from right), June Andronick and Gerwin Klein.
You can read more about the CDDC on the following blog post which was written when we previously won three iAwards at the state level for South Australia back in June.
I'm very happy to announce that the Special Issue on Verified Information Flow Security of the Journal of Computer Security (Volume 25, issue 4-5) has just been published. For this special issue I was honoured to act as Guest Editor alongside Andrei Sabelfeld and Lujo Bauer. If you're interested in what kinds of security guarantees can be provided by platform enforced (and often formally verified) information flow control, this special issue is a good place to start, covering practical systems from new hardware architectures and hypervisors to new programming languages and distributed systems. You can read more about the special issue and its contents in the freely-available foreword [Journal of Computer Security, Guest Editorial ].
I'm honoured to be a part of the team behind the Cross Domain Desktop Compositor (CDDC) [Annual Computer Security Applications Conference (ACSAC) 2016 ], which last night won three SA iAwards. The CDDC was named the South Australian:
The CDDC is a joint collaboration between Data61 and DST Group that Kevin Elphinstone and I, in our Data61 capacities, established with Mark Beaumont and Chris North of DST Group's Active Security Technologies Group. Massive credit to Mark Beaumont who conceived much of the CDDC's original design, for whom this marks his second success at the iAwards after a win in 2014 with the Digital Video Guard.
You can read more about the CDDC and the win on our official blog post.
'm currently recruiting a researcher (a postdoc or graduate) to work on the application of concurrent separation logic for verifying information flow security of seL4-based, security-critical embedded systems. Verified information flow security has seen something of a renaissance over the past 5 years, with success stories such as seL4 or the more recent mCertiKOS; but concurrency remains an open challenge and one that this project aims to address for the first time.
Are you a PhD student looking for early feedback on your work on computer security and formal methods? Please consider submitting to FCS 2017, on whose Program Committee I'm serving. FCS is, as usual, taking place at CSF 2017 (on whose PC I'm also serving), this year in Santa Barbara, co-located with Crypto 2017. FCS 2017 will be an excellent opportunity to interact with, and get exposure in, a large community of the world's best researchers in security foundations.
I was invited to the Cyber in Business Conference to speak on the University Leaders panel, around Cybersecurity education in Australian universities. Somewhat in contrast to my colleagues on the very well-informed and broad panel (Matthew Warren of Deakin; Sara Smyth of La Trobe; and Nalin Asanka of UNSW Canberra) I emphasised the importance of strong teaching in computer science fundamentals to underpin cybersecurity education: developers who don't understand how a C compiler works cannot expect to write secure C code, for instance. The conference was a lot of fun and is slated to run next in Sydney in 2017 before returning to Melbourne.
As part of its fantastic Summer Scholarships program, Data61 is offering five summer scholarships to University of Melbourne Department of Computing and Information Systems (CIS) students for the 2016/17 summer, valued at $5,000 each. The scholarships are to work on projects aligned with Data61's research interests. I'm lucky enough to be advertising three projects, related to rigorous security.
Applications close on Tuesday November 1st 2016, 11:59pm. For more details, including eligibility and the list of projects on offer, click: HERE.
Our paper on the The Cross Domain Desktop Compositor (CDDC) will appear at the 2016 Annual Computer Security Applications Conference (ACSAC). It describes a hardware prototype of the CDDC, a cross domain device that through clever design maximises both security and usability, and a formal proof of information flow security for its design. This work was carried out in collaboration with researchers from Australia's Defence Science and Technology Group (DST Group), where the CDDC was first conceived. The CDDC demonstrates, contrary to accepted wisdom, that security and usability need not be in conflict and that through careful design the two can reinforce each other.
Students who are interested in programming languages, program analysis and security: PLAS 2016, co-located with ACM CCS 2016 in Vienna, is fortunate enough to be offering travel scholarships, thanks to the generous support of our sponsors. Applications are due by October 7, so get yours in now! See the PLAS website for details.
My fantastic PhD student Sidney Amani just completed his successful thesis examination, and will soon be admitted to the degree of PhD by the University of New South Wales. Sidney's thesis, A Methodology for Trustworthy File Systems , demonstrates how to meaningfully reduce the cost of producing mission-critical, formally verified software (in this case file systems) by pursuing aggressive modular decomposition, enabling modular verification, and by programming them in pure functional languages, which naturally support straightforward forms of reasoning. My most heartfelt congratulations to Sidney!
To provide a place for less formal news, ramblings, rants and other trivia, I've started blogging at: verse.systems/blog. The first post there touches on the challenges of good software engineering teaching, and why it must be underpinned by a deep appreciation of computer science. Go check it out!
Our work on the Cogent project will appear at ICFP and ITP 2016. The Cogent language is described in detail in our ICFP paper , while the part of its verifying compiler that generates the final C code is described in the ITP paper .
My two very talented students from UNSW, Rob Sison and Ed Pierzchalski, have just had their first paper accepted, at CSF 2016. With Christine Rizkallah at NICTA, this paper presents the first theory able to verify concurrent programs that must keep confidential information secret from attackers, where the secrecy of data can depend on other data in the system. Importantly, this theory can not only verify the security of such programs but also whether they have been securely compiled, for instance whether a compiler has inadvertently introduced any timing leaks by performing optimisations that depend on secret data. We hope this theory will pave the way to verifying entire concurrent systems as being information flow secure.
I've moved to the University of Melbourne, after six wonderful years at NICTA leading its work on verified security in the Trustworthy Systems research group. I'll still be collaborating with the TS group, but am on the lookout for keen students to work with at Melbourne who are interested in how to build highly secure systems. Check out my page for Prospective Research Students.
The PLAS 2016 website with call for papers is now live. Interested in how programming languages can help improve security, or how to better analyse programs to make sure they are secure? Why not consider submitting. This year PLAS has a special focus on short papers likely to stimulate discussion and debate. Got a visionary proposal or a controversial idea? Submit it here.
My PhD student Sidney Amani is lead author on our upcoming paper at ASPLOS 2016, which reports on his work building verified file systems using verifying domain specific languages. This work was carried out as part of NICTA's Cogent project, and includes Liam O'Connor who I'm also supervising with Gabi Keller.
I and Deian Stefan are Program Committee chairs for PLAS 2016. Stay tuned for further details.
I'm serving on the Program Committee for CRTS 2015 (the International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems). CRTS will be co-located with RTSS. If you work on compositionality in the context of real-time embedded systems, please consider submitting!
I am Program Co-Chair of the Systems Software Verification Conference (SSV) 2015, which is being held on the Gold Coast (co-located with ICECCS 2015), December 7-8 2015. If your work involves rigorous or formal verification of systems software, please consider submitting! The Call for Papers is out now.
I finally got around to writing a proper website. Enjoy!