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.

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.

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.

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.

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.

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.

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.

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 Theregister.co.uk and Securityweek.com.

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.

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.

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.

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.

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.

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.

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.

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.