News Archive

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!