Southern Summer School on
Systems and Software Security

Day 1: 23 January 2023
9:00–9:50 Registration
9:50–10:00 Welcome
10:00–11:00 Gernot Heiser TS, UNSW seL4 Microkernel: Unbeatable Security and Unbeaten Performance
11:00–12:00 Shaanan Cohney U Melbourne In Crypto We Trust
12:00–13:30 Lunch
13:30–15:00 Student Session
William Kosasih U Adelaide The Gates of Time: Improving Cache Attacks with Transient Execution
Joel Kuepper U Adelaide CryptOpt: Automatic Optimization of Straightline Code
Zhuoqun Huang U Melbourne Robust malware detection via Randomized Deletion
15:00–15:30 Break
15:30–16:30 Student Session
Sioli O'Connell U Adelaide Pixel Thief: Exploiting SVG Filter Leakage in Web Browsers
Robbie Dumitru U Adelaide The Impostor Among US(B): Off-Path Injection Attacks on USB Communications
16:30–17:00 Yuval Yarom U Adelaide TBD
Day 2: 24 January 2023
9:00–10:30 Student Session
Alex Rohl DSTG & U Adelaide The State of Automated Protocol Reverse Engineering
Rui Qi Sim U Adelaide RSA Key Recovery from Digit Equivalence Information
Stuart Webb U Melbourne Adapting the Pony language onto the seL4 microkernel - In search of a capability-focused microkernel programming interface
10:30–11:00 Break
11:00–12:00 Ivan Velickovic TS, UNSW seL4 Core Platform: simplifying secure and performant systems
12:00–13:30 Lunch
13:30–14:30 Peter Schwabe MPI-SP & Radboud Engineering High-Assurance Crypto Software
14:30–15:15 Scott Buckley TS, UNSW Verifying Time Protection for seL4
16:00–Late BBQ
Day 3: 25 January 2023
9:30–10:00 Rob Sison U Melbourne & TS, UNSW Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs
10:00–11:00 Thuan Pham U Melbourne Effective Security Testing with Fuzzing: Challenges and Proposed Solutions
11:00–11:30 Break
11:30–12:30 Johannes Åman Pohjola TS, UNSW A Bluffer's Guide to the CakeML Ecosystem

Invited Talks

Gernot Heiser
Trustworthy Systems, UNSW
Title: seL4 Microkernel: Unbeatable Security and Unbeaten Performance
Abstract: in 2009 seL4, developed by the Trustworthy Systems group (TS) at was then NICTA, became the world’s first operating system (OS) kernel with a formal, machine-checked proof of functional correctness – bug-freedom in a very strong sense. TS followed this by proofs of translation correctness (extending functional correctness to the binary code), proving security enforcement, and bounds on worst-case latencies of kernel operations. At the same time, seL4 outperforms any other microkernel. This talk will provide an overview of seL4 and its verification, and discuss real-world deployments. It will outline current research on seL4 and the work on seL4-based provably-secure operating systems.
bio: Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney. His research interest are in operating systems, real-time systems, security and safety. His research vision is to completely change the cybersecurity game from playing catch-up with attackers to systems that are provably secure. As leader the Trustworthy Systems group, he pioneered large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being used in real-world security- and safety-critical systems.
Heiser's former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and is deployed on the secure enclave of all iOS devices. He presently serves as Chief Scientist of Neutrality, and Chairman of the seL4 Foundation. Gernot is a Fellow of the ACM, the IEEE, the Australian Academy of Technology and Engineering (ATSE) and the Royal Society of New South Wales (RSN). He is also an ACM Distinguished Lecturer.
Ivan Velickovic
Trustworthy Systems, UNSW
Title:seL4 Core Platform: simplifying secure and performant systems
Abstract: seL4 is a formally verified microkernel designed for making systems that require security, performance and high assurance. The seL4 Core Platform leverages seL4 to provide a lightweight operating system environment. It is designed to make building secure performant systems using seL4 significantly easier, while providing minimal abstractions. The seL4CP is intended for systems with a static architecture but also offers limited dynamicisim, making it ideal for use in embedded cyber-physical devices. The talk will provide an overview on the seL4CP and its concepts, the (in-progress) formal verification story for the seL4CP, and finally an overview of the seL4 Device Driver Framework, a framework built on top of the seL4CP for building secure and performant device drivers.
Bio: Ivan Velickovic is a junior operating systems engineer at the Trustworthy Systems research group at UNSW Sydney. His current work is primarily on virtualisation and device drivers on seL4. His current goal is to use and develop a minimal OS on top of seL4 called the seL4 Core Platform to enable reliable and performant virtual machines and device drivers. Prior to this work, Ivan completed his Bachelor's in Computer Science at UNSW Sydney.
Johannes Åman Pohjola
Trustworthy Systems, UNSW
Title:A Bluffer's Guide to the CakeML Ecosystem
Abstract: From humble beginnings in 2012 as a mostly fictional aside in a paper about program synthesis, the CakeML programming language is now one of the landmark success stories in formal verification. It features an end-to-end verified optimising compiler targeting both mainstream and boutique architectures, and a rich ecosystem of program verification tools and sister languages. This presentation will give you an overview of what's what and what's cooking.
Peter Schwabe
MPI-SP and Radboud University
Title: Engineering High-Assurance Crypto Software
Abstract: In this talk I will introduce the jasmin programming language and explain how implementing cryptographic software in jasmin helps improve confidence in correctness and security without compromising on performance.
bio: Peter Schwabe is research group leader at MPI-SP and professor at Radboud University. He graduated from RWTH Aachen University in computer science in 2006 and received a Ph.D. from the Faculty of Mathematics and Computer Science of Eindhoven University of Technology in 2011. He then worked as a postdoctoral researcher at the Institute for Information Science and the Research Center for Information Technology Innovation of Academia Sinica, Taiwan and at National Taiwan University.
His research area is cryptographic engineering; in particular the security and performance of cryptographic software. He published more than 60 articles in journals and at international conferences presenting, for example, fast software for a variety of cryptographic primitives including AES, hash functions, elliptic-curve cryptography, and cryptographic pairings. He has also published articles on fast cryptanalysis, in particular attacks on the discrete-logarithm problem. In recent years he has focused in particular on post-quantum cryptography. He co-authored the "NewHope" and "NTRU-HRSS" lattice-based key-encapsulation schemes which were used in post-quantum TLS experiments by Google and he is co-submitter of seven proposals to the NIST post-quantum crypto project, all of which made it to the second round, five of which made it to the third round, and 3 of which were selected after round 3 for standardization.
Rob Sison
University of Melbourne and Trustworthy Systems, UNSW
Title:Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs
Abstract: Software does not always have the luxury of limiting itself to single-threaded computation with resources statically dedicated to each user to ensure the confidentiality of their data. That being the case, what techniques would it take to prove formally (1) that programs enforce confidentiality in the face of the mixed-sensitivity reuse of resources and the concurrency so often employed to make them scale; and (2) that a compiler won’t break that enforcement? This talk will give a high-level overview of the contributions of my 2020 doctoral dissertation Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs, in which I posed the thesis that these sorts of proofs are feasible, using the seL4 component-based software design of the Cross Domain Desktop Compositor as a case study.
Bio: Rob is a postdoctoral researcher for the University of Melbourne and visiting fellow with UNSW Sydney whose current research focus is the seL4 time protection verification project. More broadly, Rob is interested in all applications of interactive theorem proving, as well as anything to do with the design and construction of software systems with formally proved functional-correctness and security properties at scale. After a 5-year early career stint (2008-2014) as an OS-level programmer with NICTA spin-out Open Kernel Labs (including post-acquisition by General Dynamics), Rob returned to UNSW to pursue postgraduate studies in computer security and formal methods. Their doctoral thesis with UNSW then focused on the practical application of formal methods for proving and preserving concurrent value-dependent notions of noninterference, the strictest kind of confidentiality property. Rob was co-recipient of the 2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia with co-entrants Toby Murray (University of Melbourne) and Mark Beaumont (DSTG) for research contributions to the Cross Domain Desktop Compositor.
Scott Buckley
Trustworthy Systems, UNSW
Title:Verifying Time Protection for seL4
Abstract: Microarchitectural timing channels are a well-known mechanism for information leakage. "Time protection" has recently been demonstrated as an operating system mechanism able to prevent them. In seL4 we have developed an implementation of time protection that prevents microarchitectural timing channels by selectively partitioning key microarchitectural state either spatially or temporally. This approach has been formally verified for an operating system that meets certain well-defined requirements, and we have developed a proof approach for verifying that the seL4 microkernel meets those requirements. In this talk we will discuss our timing protection mechanisms, why we know they work, and examine a high-level view of how we are verifying that seL4 implements them correctly.
Bio: Scott is a postdoctoral fellow at the University of New South Wales, working in the Trustworthy Systems team on formal verification for seL4. Specifically, he works on time protection: modeling microarchitectural state behaviour and proving that seL4's time protection mechanisms prevent leaks through time-based microarchitectural side channels. Prior to this work Scott completed his PhD in programming languages and formal methods at Macquarie University, Sydney.
Shaanan Cohney
University of Melbourne
Title: In Crypto We Trust
Abstract: Mom, dad, and your babysitter all ask you if they should buy "crypto". Investors at both the small and the big end of town are seemingly caught up in the craze. Cryptographers and entrepreneurs are busy collaborating on the latest and greatest distributed systems to fix issues with trust in financial systems and products. Yet, crypto schemes keep going bust. Is this just a teething problem? Is this a technical problem? Is it only a few bad actors bringing grifts, scams, and vaporware? Or are the consumer protection challenges more fundamental?
The talk will critically and empirically examine the effectiveness of socio-technical solutions from the crypto community---open-sourcing protocols and “coding-in” governance. Afterward I'll present an analysis of what the law might do to help resolve disputes.
This talk is aimed to please both the hardest sceptics and the most ardent believers in blockchains.
bio: Shaanan Cohney is a Lecturer at the University of Melbourne and a Visiting Assistant Professor at the University of Pennsylvania. His research area is at the intersection of Computer Security and Law where he focuses on technology to product consumers and businesses. Shaanan's past experience includes placements as a Cybersecurity Fellow in the office of U.S Senator Ron Wyden, and in the Office of Policy Planning at the Federal Trade Commission. His work has received multiple awards from both research and industry, including Best Paper at ACM CCS and an Pwnie Award for best Cryptographic Attack. He is also the recipient of the Excellence in Tutoring and Excellence in Teaching Awards at the University of Melbourne.
Shaanan holds a PhD and Masters in Law from the University of Pennsylvania, and completed a postdoctoral fellowship at Princeton University.
Thuan Pham
University of Melbourne
Title: Effective Security Testing with Fuzzing: Challenges and Proposed Solutions
Abstract: Thorough testing is essential to increase the security of software systems and fuzzing (i.e., fuzz testing) is one of the most popular and effective approaches. However, the technique has several (open) challenges as discussed in the Shonan meeting No. 160 on Fuzzing and Symbolic Execution, which was organized by Marcel Böhme, Cristian Cadar, and Abhik Roychoudhury in Tokyo in September 2019. In this talk, we will revisit these challenges and discuss some solutions that have been proposed and (partially) implemented by our Cyber Security group at the University of Melbourne. We will also share the limitations of these approaches and open discussions for future research.
Bio: Thuan Pham is an ARC DECRA fellow and lecturer in Cyber Security at the University of Melbourne (UoM). He received his Ph.D. degree in Computer Science from the National University of Singapore in July 2017. He has been working on scalable and high-performance fuzz testing to improve the reliability & security of software systems. His research, in collaboration with companies and government agencies, has led to many papers published at premier venues (e.g., TSE, ICSE, ASE, ISSTA, CCS), one U.S. patent, and one Australian provisional patent. He has developed several open-source tools for automated security testing (e.g., AFLGo, AFLSmart, AFLNet, AFLTeam) that are responsible for 100+ (critical) vulnerabilities discovered in large real-world software systems. His research has been featured on media channels like and

Student Talks

Alex Rohl
DSTG and the University of Adelaide
Title: The State of Automated Protocol Reverse Engineering
Abstract: Messages sent on computer networks are encoded using engineered protocol specifications. However, such descriptions may not be available or only exist as verbose documents due to the proprietary nature of new protocols. This is a problem because protocol specifications are necessary for building an Intrusion Detection System (IDS) that can monitor system behaviour and therefore provide situational awareness, such as the presence of malicious activity. The Automated Protocol Reverse Engineering (APRE) field of research aims to create models to infer the message format of each packet from an unspecified protocol. The existing literature has focussed on unsupervised methods, which have seen limited success due to the lack of annotated data and the constraints on the fidelity of outputs. In particular, the lack of annotated data makes it difficult to measure a model’s generalisability to new protocols.

Mr Rohl will introduce a review of the APRE literature and explain the required dataset framework and current steps implemented to further the APRE field.

Joel Kuepper
University of Adelaide
Title: CryptOpt: Automatic Optimization of Straightline Code
Abstract: The manual engineering of high-performance implementations typically consumes many resources and requires much in-depth knowledge of the hardware. Compilers try to address these problems; however, they are limited by design in what they can do. To address this, we present CryptOpt, an automatic optimizer for long pieces of straightline code. Experimental results across eight hardware platforms show that CryptOpt achieves a speed-up factor of up to 2.56 over current off-the-shelf compilers.
Robert Dumitru
University of Adelaide
Title: The Impostor Among US(B): Off-Path Injection Attacks on USB Communications
Abstract: USB is the most prevalent peripheral interface in modern computer systems and its inherent insecurities make it an appealing attack vector. A well-known limitation of USB is that traffic is not encrypted. This allows on-path adversaries to trivially perform man-in-the-middle attacks. Off-path attacks that compromise the confidentiality of communications have also been shown to be possible. However, so far no off-path attacks that breach USB communications integrity have been demonstrated.

In this work we show that the integrity of USB communications is not guaranteed even against off-path attackers. Specifically, we design and build malicious devices that, even when placed outside of the path between a victim device and the host, can inject data to that path. Using our developed injectors we can falsify the provenance of data input as interpreted by a host computer system. By injecting on behalf of trusted victim devices we can circumvent any software-based authorisation policy defences that computer systems employ against common USB attacks. We demonstrate two concrete attacks. The first injects keystrokes allowing an attacker to execute commands. The second demonstrates file-contents replacement including during system install from a USB disk. We test the attacks on 29 USB 2.0 and USB 3.x hubs and find 14 of them to be vulnerable.

Rui Qi Sim
University of Adelaide
Title: RSA Key Recovery from Digit Equivalence Information
Abstract: The seminal work of Heninger and Shacham (Crypto 2009) demonstrated a method for reconstructing secret RSA keys from partial information of the key components. In this paper we further investigate this approach but apply it to a different context that appears in some side-channel attacks. We assume a fixed-window exponentiation algorithm that leaks the equivalence between digits, without leaking the value of the digits themselves.

We explain how to exploit the side-channel information with the Heninger-Shacham algorithm. To analyse the complexity of the approach, we model the attack as a Markov process and experimentally validate the accuracy of the model. Our model shows that the attack is feasible in the commonly used case where the window size is 5.

Sioli O'Connell
University of Adelaide
Title: Pixel Thief: Exploiting SVG Filter Leakage in Web Browsers
Abstract: Pixel stealing attacks provide a malicious website with a view into the content of a victim website, breaking cross-origin isolation and potentially violating web user privacy. Filter-based attacks are one form of this attack class, which exploit differences in filter execution times depending on the content of the filtered images. To protect against such attacks, browser vendors have modified filter operations to remove observable timing differences.

In this work we show that this protection is not enough. We mount a cache side-channel attack and show how a web-based attacker can monitor data-dependent memory accesses during filter execution to recover the contents of filtered images. We demonstrate two practical applications of our pixel stealing attack, an attack which leaks text-based content from an embedded webpage and an attack which recovers part of the victim's browsing history.

Stuart Webb
University of melbourne
Title: Adapting the Pony language onto the seL4 microkernel - In search of a capability-focused microkernel programming interface
Abstract: The seL4 microkernel provides one of the highest levels of security assurances possible for an operating system via its machine-checked proofs of properties such as integrity, authority confinement, and information-flow non-interference. The key mechanism underlying these proofs and assurances is its capability system for resource management, which is used to describe all memory and communication channels between user-level components of an seL4 system.

Object Capability programming languages make similar use of a capability security model for expressing authority propagation throughout code. In these languages, object references are viewed as the capabilities, such that having a reference to an object represents the rights to use and control that object, with the assumption that object references cannot be invented or forged (for example by dereferencing arbitrary memory addresses). Security mechanisms and policies can become expressed through object-oriented programming patterns such as object proxies, and execution contexts usually specify ways to be launched with initial capabilities, or channels to obtain subsequent capabilities via once the program starts.

Whilst many tools have been developed for building systems with seL4 such as capDL and CAmKES, they rely on static distribution of capabilities upfront at project build time, and in general do not provide for dynamic capability transfer once the system has started. In practice, for runtime/dynamic access control, many systems revert to standard POSIX layers where ambient authority for resource access returns, throwing out the fine-grained access control possibilities that come for free with a capability model. In theory, an object capability language would provide a better means for building dynamic capability systems, especially if such a language can have seL4 capabilities for kernel objects mapped into it.

Many Object Capability languages exist (E, Oz-E, Jessie/SES, SHILL, Pony, Dala) but their purposes/research goals are varied and their implementations can rest on many layers of software. This research surveys various object capability languages from the research community and evaluates their appropriateness for mapping to seL4. The Pony language is examined as a frontrunner for an implementation due to its C-like performance and relatively minimal set of language implementation dependencies. However many trade-offs are still involved due to the minimal mechanisms provided by seL4 (compared to more prevalent monolithic kernels), which are explored with an aim to more formally detail and compare the properties and limitations of both seL4 and object capability language capability models and mechanisms.

William Kosasih
University of Adelaide
Title: The Gates of Time: Improving Cache Attacks with Transient Execution
Abstract: For over two decades, cache attacks have been shown to pose a significant risk to the security of computer systems. In particular, a large number of works show that cache attacks provide an essential stepping stone for implementing transient-execution attacks. However, much less effort has been expended investigating the reverse direction—how transient execution can be exploited for cache attacks. In this work, we answer this question.

We first show that using transient execution, we can per- form arbitrary manipulations of the cache state. Specifically, we design versatile logical gates whose inputs and outputs are the caching state of memory addresses. Our gates are generic enough that we can implement them in WebAssembly. Moreover, the gates work on processors from multiple vendors, including Intel, AMD, Apple, and Samsung. We demonstrate that these gates are Turing complete and allow arbitrary com- putation on cache state, without exposing the logical values to the architectural state of the program.

We then show two use cases for our gates in cache attacks. The first use case is to amplify the cache state, allowing us to create timing differences of over 100 millisecond between the cases that a specific memory address is cached or not. We show how we can use this capability to build eviction sets in WebAssembly, using only a low-resolution (0.1 millisecond) timer. For the second use case, we present the Prime+Store attack, a variant of Prime+Probe that decouples the sampling of cache state from the measurement of said state. Prime+ Store is the first timing-based cache attack that can sample the cache state at a rate higher than the clock rate. We show how to use Prime+Store to obtain bits from a concurrently executing modular exponentiation, when the only timing signal is at a resolution of 0.1 millisecond.

Zhuoqun Huang
University of Melbourne
Title: Robust malware detection via Randomized Deletion
Abstract: By leveraging massive amounts of data, machine learning systems can effectively automate many cybersecurity applications, such as malware detection and intrusion detection. On the other hand, adversaries exploit the adaptive nature of machine learning to conceal their maliciousness against machine learning (ML) detection systems, hindering system performance or hiding a backdoor trigger that can be activated at will. Certified robustness is a defence mechanism that aims at providing a robustness guarantee for given inputs, and has been proven effective at preventing such attacks. While extensive research has been conducted for domains with fixed dimension data such as image recognition, certified defence for varable length sequence data such as malware or languages are still absent. Our project extends randomized smoothing, a certified defence mechanism against adversarial attacks, to the Levenshtein distance threat model. We further specialize our mechanism to the malware detection domain. Our novel mechanism can certify any sequence data against insertion, deletion and substitution operations. Experiments show that we produce meaningful certified radius with minimal impact on the model performance. To our knowledge, we are first in broadening the threat model beyond $L_p$ distances.