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.
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 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 colleages 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!