News Archive

CrowdStrike Commentary

The large-scale outage caused by CrowdStrike on July 19 has offered a unique opportunity to shed light on better ways the cyber security industry can build their software, as well as to dispel some of the misinformation that has circulated since the outage. I've written multiple pieces on these topics including:

• A technical explainer on CrowdStrike Falcon for The Conversation;
• A personal blog post to try to clear up some of the confusion immediately after the incident;
• An analysis of the tradeoffs of current EDR technologies like CrowdStrike's for The Conversation;
• A deep dive personal blog post on what went wrong and why CrowdStrike's plan is inadequate; and
• A Q&A article published in the University of Melbourne's Pursuit.

EDEFuzz wins Distinguished Paper Award at ICSE 2024

Over the past couple of years, my PhD student Lianglu Pan has been working on the first mechanical method for detecting Excessive Data Exposure (EDE) vulnerabilities in web applications. This method was devised in collaboration with Lianglu's PhD supervisors, Thuan Pham, Shaanan Cohney, and me. We're delighted to say that this work will appear at ICSE 2024. You can check out the paper online, which was recognised with a Distinguished Paper award. If you're attending ICSE, please say hi to Lianglu!

CCS 2023

I'm looking forward to attending ACM CCS 2023 where I'll be presenting the most recent outcomes of the COVERN project, in which we have developed the first proved sound methods for the auto-active verification of declassification policies for concurrent programs. This work was a long-running collaboration, the bulk of which was carried out while Mukesh Tiwari was working as a postdoc here in my group (and who recently joined Swansea University as a faculty member), and in collaboration with my ex-postdoc Gidon Ernst at LMU Munich, and David Naumann at Stevens Institute of Technology. If you're interested in learning more, I'd recommend checking out the extended version of our CCS 2023 paper or, if you happen to be in Copenhagen, drop me a line and let's meet up.

Invited Talk at ICFEM 2023

I'll be giving an invited talk at the 24th International Conference on Formal Engineering Methods (ICFEM 2023), which is taking place in Brisbane later this month. I'll be speaking about the history and recent achievements of the COVERN project, which has culminated in producing the first methods for what I call Practical Verified Concurrent Program Security (the slides for my talk).

Algovis Release

I've finally gotten around to publishing the rudimentary, interactive algorithm visualisation tool that I wrote when teaching COMP90038 - Algorithms and Complexity (2021--2022) to aid students' understanding of introductory algorithms and design techniques. The tool is called Algovis and you can get it from GitHub, including full documentation, which shows the visualisations in action.

Insecurity Separation Logic

I am delighted to announce that our long-running work to develop an automatic and compositional methods for detecting information leakage vulnerabilities in programs will appear at ICFEM 2023. This work includes not only the design of a new program logic for detecting leakage (Insecurity Separation Logic) but also the implementation of its automatic application inside two tools: our own Underflow tool, and as an extension to Meta's Infer static analyzer. All materials, plus an extended version of the paper, are available on the COVERN project website.

Welcome Aaron Bembenek!

I am delighted to welcome Aaron Bembenek who joins the CATCH MURI project as a postdoc working at the intersection of formal methods and machine learning. Aaron completed his PhD at Harvard, advised by Stephen Chong. Aaron brings a wealth of expertise, including in logic programming and automated solving.

Melbourne Business Analytics Conference - Generative AI Panel

I had a wonderful time this week talking about the relationship between generative AI and cybersecurity as part of the Navigating the Generative Frontier: The Evolution of Decision Making in the Age of AI panel at the 2023 Melbourne Business Analytics Conference. There is so much interest in this technology and much more to be done to educate organisations about how to make best use of it while avoiding its potential to increase exposure to cyber threats.

ACM Software System Award

I am honoured to be recognised amongst the 14-member team who this year was awarded the ACM Software System Award for our work on the seL4 microkernel. Quoting from what I wrote for the University of Melbourne's announcement: This marks the first time the ACM Software System Award has been awarded to an Australian-based team. The seL4 project represents two decades of sustained world-leading research. Since its original publication in 2009, the seL4 kernel has set the bar for how secure systems should be engineered, while demolishing long-held beliefs about the limits of what formal methods can achieve, demonstrating that system security need not come at the cost of performance. Long live seL4!

CSF 2024

Please consider submitting to the IEEE Computer Security Foundations Symposium (CSF) 2024. Tamara Rezk and I are Program Chairs for CSF 2024 and we warmly welcome submissions on topics at the intersection of computer security and formal foundations.

Welcome James Tobler!

I am excited to be working with James Tobler who joins my group as a Research Assistant working on automatic verification of concurrent programs, funded by DST Group. James' project focuses on how to automate concurrent program verification via Rely-Guarantee and related reasoning techniques like Owicki-Gries by automatically inferring program assertions.

FormaliSE 2023

Please consider submitting to the 2023 International Conference on Formal Methods in Software Engineering (FormaliSE). FormaliSE 2023 is taking place in Melbourne between 14--15 May, co-located with ICSE 2023. I, along with Marie-Christine Jakobs of TU Darmstadt, as Program Chairs warmly welcome submissions on topics at the intersection of formal methods and software engineering. We welcome full research papers; case study papers; and shorter research ideas papers as well. Abstracts are due on Januar 16 2023 January 9 2023, with papers due on 27 January 2023 16 January 2023. Please consider submitting.

Time Protection Formalisation Paper at FM 2023

I am delighted to announce that the first major formal methods paper arising from the seL4 Time Protection project will appear at FM 2023. The paper shows how time protection (enforcement of the absence of microarchitectural timing channels) can be formally defined for an operating systems kernel, and how a kernel implementation can in principle be proved to enforce this security guarantee. Major kudos to the two primary researchers on this project, Rob Sison and Scott Buckley.

Congratulations Dongge Liu

I am delighted to announce that my (now former) PhD student Dongge Liu successfully passed his thesis examination. Dongge's thesis, Software Testing with Monte Carlo Tree Search, examines how to apply ideas from Artificial Intelligence to the problem of automatically generating tests for programs (for instance to find vulnerabilities). Dongge's research was a wonderful collaboration involving Ben Rubinstein, Gidon Ernst, and Thuan Pham, and we look forward to future collaborations in this area.

Two Papers in Journal of Functional Programming Special Issue on Secure Compilation

Eureka Prize for Outstanding Science in Safeguarding Australia

SecRSL paper at OOPSLA 2021

Eureka Prize Finalist

HotSpot 2021, September 6 (online)

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!

Invited Talk at TVD 2021

On Wednesday September 1 I will be speaking at the first TechForum on Vulnerability Detection about our recent work on Incremental Vulnerability Detection.

F-IDE Paper: Integrating a Program Verifier with a Program Debugger

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.

Congratulations Than Nguyen!

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.

Legion at ASE 2020

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.

Welcome Robert Sison

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.

VERONICA: Open Source Release and Paper at CSF 2020

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.

Legion partakes in Test-Comp 2020

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.

New Artifact: Under-Approximate Relational Logic

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.

Welcome Mukesh Tiwari

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.

I'm Hiring: 2-year postdoc position on verified timing-channel security for seL4

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.

SecC Initial Release

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.

Understanding Ethereum's Gas Mechanism

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'm Hiring: Researcher in Verified Confidentiality for Weak Memory Models

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

FTfJP 2019 (Formal Techniques for Java-like Programs)

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!

OzCHI 2018 Work-In-Progress Paper

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.

Congratulations Dr Daniel Matichuk!

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.

OpenGov Recognition of Excellence Award for the CDDC

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.

New Paper on the Benefits and Drawbacks of Proofs for Secure Software

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.

Welcome Gidon Ernst

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.

COVERN: Open Source Release and EuroS&P

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):

• The COVERN logic: a program logic for compositionally verifying information flow security of shared-memory concurrent programs,
• The COVERN compiler: a proof of concept, formally verified compiler for shared-memory concurrent programs, that provably preserves information flow security (i.e. ensures that the compiled program does not leak information, if the source program was verified as secure in the COVERN logic).

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 Dr Yude Lin!

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.

Overcoming Adversity in Graduate Research

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.

CDDC Wins 2 National iAwards

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: Research and Development Project of the Year, and Infrastructure and Platforms Innovation of the Year. 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.

Special Issue of Journal of Computer Security on Verified Information Flow Security

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

CDDC wins 3 SA iAwards

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: Research and Development Project of the Year, Infrastructure and Platforms Innovation of the Year, and Public Sector and Government Markets winner. 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.

I'm Hiring a researcher in Program Verification and Security

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

Click here for more information.

FCS 2017 with CSF and Crypto 2017

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.

Cyber in Business Conference - University Leaders Panel

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.

Data61-UoM Summer Scholarships

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.

Cross Domain Desktop Compositor at ACSAC 2016

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.

PLAS 2016 Travel Grants Due October 7th

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.

Congratulations Dr Sidney Amani!

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!

I've Started Blogging

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!

Cogent at ICFP and ITP 2016

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 .

Archive of Formal Proofs

To coincide with CSF 2016, the Isabelle theories that accompany our CSF 2016 paper are now available in the Archive of Formal Proofs (AFP). Check out the two AFP entries:

• A Dependent Security Type System for Concurrent Imperative Programs
• Compositional Security-Preserving Refinement for Concurrent Imperative Programs

CSF 2016

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.

University of Melbourne

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.

PLAS 2016 Call for Papers

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.

ASPLOS 2016

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.

PLAS 2016

I and Deian Stefan are Program Committee chairs for PLAS 2016. Stay tuned for further details.

CRTS 2015

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!

SSV 2015

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.

New Website

I finally got around to writing a proper website. Enjoy!