Schedule

For the first lecture, I will talk about the benefits of type- and spatial-safety as a means of ruling out memory-based attacks. I will talk about ongoing work on the Checked C project that aims to retrofit C programs to be spatially safe, incrementally. I will also talk about my prior work on the Cyclone programming language that aimed to avoid temporal safety violations (e.g., "use after free"). This work is now reflected in many ways in the Rust programming language.

For my second lecture, I will talk about random (or "fuzz") testing, which aims to find bugs in insecure programs. This is a complementary technology to Checked C, for the parts of the program not protected by Checked C's checks. Fuzzers appear to be very successful at finding bugs, so it's important to understand why they work. Unfortunately, the existing research literature does not provide uniformly good scientific evidence on this front. We surveyed the recent research literature and assessed the experimental evaluations carried out by 32 fuzzing papers. We found problems in every evaluation we considered. We then performed our own extensive experimental evaluation using an existing fuzzer. Our results showed that the general problems we found in existing experimental evaluations can indeed translate to actual wrong or misleading assessments. We developed some guidelines, and open problems, that may address these issues.

S2E is a platform for in-vivo analysis of software systems that combines a virtual machine with symbolic execution. Users install and run in S2E an unmodified software stack, including programs, libraries, the OS kernel, and drivers. Symbolic execution then automatically explores thousands of paths through the system, allowing users to check desired properties even in corner-case situations and at any level of the software stack. S2E works on unmodified binaries, does not require writing code in special languages, or model the environment.

In this tutorial, you will learn how to use S2E to find bugs and vulnerabilities in Windows applications and device drivers. In the first part of the tutorial, you will learn the basics of symbolic execution with S2E with hands-on testing of Windows applications. In the second part of the tutorial, we will cover Windows kernel driver testing and show how S2E can help you build well-tested drivers with robust error recovery code using symbolic fault injection. You will try integrated code coverage tools and profilers to quickly diagnose symbolic execution bottlenecks, which you will then resolve with techniques such as state merging and function modeling. Finally, we will show how to automatically generate proofs of vulnerabilities with S2E.

To follow this tutorial optimally, you will need a Windows installation (either in a VM or native) with Visual Studio 2017 and the Windows Driver Kit version 1709. You will use that to hack and build the sample drivers we provide. We will provide remote access to Linux machines with S2E and guest images pre-installed. You may of course install S2E and build the Windows images on your own machine ahead of time if you wish, it’s fully automated.

Symbolic analysis of programs have been first studied for the purpose of program verification. In recent decades, symbolic execution technology has witnessed renewed interest due to the maturity of Satisfiability Modulo Theory (SMT) solvers. Powerful dynamic analysis tools have leveraged the back-end solvers to systematically navigate large search spaces leading to application of symbolic analysis in test generation or vulnetrability detection. In this tutorial, we will first study the power of state-of-the-art symbolic execution based approaches for various security vulnerability analysis tasks such as finding zero-day vulnerabilities and/or crash reproduction. We compare the symbolic analysis approaches to grey-box fuzz testing approaches (which are routinely employed in industrial settings). Through such comparison, we can try to understand the state-of-practice of symbolic execution in terms of its ability to detect software vulnerabilities.

In the later part of the tutorial, we will conceptualize the use of symbolic execution approaches/tools for purposes beyond guiding search. We will sketch the usage of symbolic execution in inferring specification of intended program behavior. This is done by analyzing a buggy program against selected tests. Such specification inference capability can be combined with program synthesis techniques to automatically repair programs. Automated program repair via symbolic execution goes beyond search-based approaches which lift patches from elsewhere in the program. Such an approach can construct “imaginative” patches, serves as a test-bed for the grand-challenge of automated programming, and contributes to the vision of self-healing software.

Applications written in C++ are prone to memory corruption and type confusion vulnerabilities as the C++ programming language enforces neither memory nor type safety. Memory corruption is caused, e.g., by buffer overflows or using already freed memory. Type confusion happens if the runtime type of an object differs from the statically expected type due to an incorrect type cast. Type casting is a core feature of C++ that enables modularity but for performance, the majority of casts are only checked statically at compile time due to the expense of the C++ runtime type checking mechanism.

Due to such low level errors, applications can be vulnerable to exploits which allow an adversary to escalate privileges, execute arbitrary code, leak information, or simply cause denial of service to legitimate requests. The two fundamental approaches to secure software are either finding and fixing the underlying bugs or to mitigate the effects of vulnerabilities.

In the first session, we will focus on bug finding techniques using compiler-based instrumentation. To discover type safety violations, and thereby protect against type confusion vulnerabilities. We introduce HexType, a mechanism that enforces type safety for C++. HexType makes all type casts explicit. Upon allocation, metadata is recorded for each newly created object. Each cast, explicit, implicit, or static results in a runtime check using the recorded metadata. Type violations result in program termination. Our type safety mechanism integrates into existing testing frameworks or can be combined with a fuzzing framework to discover new vulnerabilities.

Even with substantial fuzzing efforts, some bugs will remain undiscovered. In the second session, we will discuss compiler-based mitigations. We have developed a mechanism to protect against control- flow hijacking attacks that leverages the unique properties of C++ to augment existing Control-Flow Integrity (CFI) mechanisms. CFI is an upcoming mitigation that is already deployed on Google Chrome and Microsoft Edge and at the verge of wide deployment. CFI measures, for each call site, the set of allowed targets using a static analysis. At runtime, the actual value is compared to the allowed targets, terminating at a miscompare. The static analysis is prone to over- approximation. We propose to make the analysis dynamic by guaranteeing the integrity of object types at runtime, thereby improving the precision of the analysis and protecting against a set of code reuse attacks that CFI would miss.

The vast majority of code running on computing platforms is written in C/C++ or running on a VM which itself is written in one of these languages. So-called safe languages that employ PL-based security have proven to be less secure than hoped: because it had become a vector for attack, Apple stopped shipping the Java VM with Mac OS X, and another ostensibly safe language, JavaScript, has been the subject of numerous attacks. Defending against exploits in depth requires approaches to harden C and C++ code, ideally without the need for rewriting code and without imposing significant performance penalties.

The original attacks on C/C++ applications depended on "smashing" the stack; because modern compilers include effective and cheap countermeasures to stack-smashing attacks, the focus of this lecture is on the heap, which is much more complex and expensive to protect. In this class, I will explain a range of heap-based attacks and how they interact with existing runtime systems and memory managers. I will talk about the challenges of coping with these issues, and describe our DieHard/DieHarder systems, which leverage randomization and novel allocation algorithms to efficiently and provably reduce the vulnerabilities of C/C++ applications to a wide class of heap-based attacks; this work directly inspired reliability and security enhancements in Microsoft Windows. I will talk about how these techniques enable self-healing from attack via statistical inference, and describe recent advances that further close the performance gap between unprotected and protected code while providing a high degree of protection.

Cyber attacks are becoming increasingly targeted and stealthy. For example, advanced targeted attacks (also called advanced persistent threats or APTs) tend to be stealthy, low-and-slow, and sometimes disguised via psychosocial campaigns. Such trends in cyber attacks call not only for proactive technologies that prevent or deter attacks, but also reactive technologies that detect and investigate ongoing or finished attacks.

In this mini-course, we focus on the investigation – or forensics – of cyber attacks, with the goals of (i) understanding the intent, strategy, and detailed steps and targets of an attack, (ii) collecting various types of evidence for possible legal proceedings, (iii) revealing hidden impacts of an attack to minimize loss and to prevent similar attacks in the future. We will cover two kinds of cyber forensics techniques: (1) temporal forensics involves analyzing log data to identify events related to an attack and their causal relations; and (2) memory forensics involves analyzing the memory snapshot of a system to extract critical information. Students will get a chance to learn the state-of-the-art and conduct labs on realistic attack forensics.

Binary translation, analysis and recompilation with McSema.

We will look at traditional ways of obfuscating code, i.e. ways to make software harder to understand and analyze. There will be a significant hands-on practical component to this part of the course, where we will obfuscate code using automatic tools.

In the first part of this lecture, we will study some of the most powerful reverse engineering attack methods, including methods deployed today by professional hackers and state-of-the-art academic methods such as fuzzing, pointer chaining, pattern matching, symbolic execution, statistical attacks, and generic de-obfuscation techniques.

In the second part, we will present results from experiments with various kinds of attackers that help us to understand how the different techniques are combined into full fledged attacks.

In the third part, will discuss some defenses against some of the advanced attacks, such as more advanced obfuscations, but also anti-taint techniques, anti-debugging techniques, anti-tracing techniques, anti-tampering techniques, and code renewability.

Virtual machines (PVMs) are often used to provide software protection. In this tutorial, we discuss the role and power of process-level virtual machines (PVMs) in software protection. The key advantage of PVMs is that they support efficient run-time transformations of the code to be protected. When used in combination with other software protection techniques such as white-box cryptography, guard networks, opaque predicates, etc., PVMs force the attacker to perform resource-intensive dynamic analysis. The tutorial discusses how efficient process-level virtual machines are constructed and how they are used to thwart both static and dynamic analyses by crackers through application of several novel transformations enabled by PVMs.

The second talk will focus on DARPA's Cyber Grand Challenge (CGC), which was announced in November 2013. The challenge was to build an autonomous cyber reasoning system that could analyze software, identify vulnerabilities, formulate patches and deploy them on a network all in real time. To test these capabilities, the cyber reasoning systems would face off against each other in a cyber version of capture the flag (CTF) with the winning team receiving a $2M cash prize. 104 teams from across the world entered the competition and began designing and building the supercomputers necessary to compete. In this talk I will describe the CGC competition, present some of the unique challenges faced by the teams, and provide an overview of technologies used to address these challenges. I will also present detailed analysis of the telemetry collected during the CGC final event. The talk will conclude by describing a new program spawned by CGC, CHESS (Computers and Humans Exploring Software Security), and some its unique challenges.

While the digital world connects devices, peoples and things in a speed beyond humans’ imagination, hostile digital environments have been becoming more dominated from consumer devices to home networks, to the public Internet, to the cloud and web services, and to the Internet of Things, where traditional security models are inadequate to address emerging threats and attacks. The anything/anytime/anywhere properties of modern connectivity make software security and digital asset protection much more challenging and critical.

This lecture is to discuss trends in threats and security paint points, new challenges to information security, white-box software attack scenarios, introduce software security immunity and security patterns (that are abstracted from many application domains in terms of use cases, vulnerability and threat analysis, and security solutions), and security lifecycle of digital applications mandating protection from creation and development, through distribution and then ultimately consumption from being deployed and maintained in the field. Moreover, we introduce homomorphic obfuscation technology and detail certain software protection technologies currently available in markets as a guide to the state of the art. Finally, we will brief AI and ML security problems and real challenges to cyber-security on connected and intelligent vehicles.

Preventing unauthorised information flow in computer systems is a problem that has been recognised at least since the 1970s, and is still not solved satisfactorily. With the move from time-shared central computers to personal computing platforms interest in the topic has waned, until the shared-platform model re-emerged in the form of public clouds, as well as mobile devices running a large number of apps from untrustworthy sources. This has put information-flow security, and especially covert information flows, back on the agenda.

The last decade saw significant progress in fundamental approaches to computer security, especially with the seL4 microkernel, the first operating system with a formal proof of implementation correctness. Subsequent work proved information-flow properties about seL4, including its ability to prevent information flow through covert storage channels. This leaves timing channels as the major security threat that must be resolved.

In this talk I will present an introduction on seL4 and its main concepts, and give an overview of its verification story and the information security challenges it does and does not address. I will explain some of the challenges presented by the present programming model of computer systems, with the instruction-set architecture (ISA) as the hardware-software contract. I will argue that the ISA abstracts too much for security, and how it could be refined into a contract that makes it possible to reason about the absence of timing channels. I will also talk about work in progress on mechanisms that allow seL4 to prevent information leakage through timing channels, in a way that should be verifiable against a suitable hardware-software contract.

Speculative execution is a processor design feature that improves performance by prematurely executing instructions based on a prediction that these will be required by the running program. The recently published Spectre and Meltdown attacks show that misprediction of the instructions to be executed can result in devastating information leaks, which can completely erode the confidentiality offered by hardware protection mechanisms. This talk describes some of the published speculative execution attacks, including their cause, exploitation techniques, and countermeasures.

The Parfait static code analysis tool focuses on detecting vulnerabilities that affect C, C++, Java and PL/SQL languages. Its focus has been on four key items expected of a commercial tool that lives in a commercial organisation:

• precision of results (i.e., high true positive rate),
• scalability (i.e., being able to quickly scan millions of lines of code),
• incremental analysis (i.e., run over deltas of the code quickly), and
• usability (i.e., ease of integration into standard build processes and reporting).

Parfait is used everyday around the world by thousands of Oracle developers.

In this presentation, we’ll sample a flavour of Parfait. We explore some real-world challenges faced in the creation of a robust vulnerability detection tool, we look into two examples of vulnerabilities that severely affected the Java platform in 2012-13 and most machines in 2017-18, and we conclude by recounting what matters to developers for integration into today’s continuous integration and continuous delivery (CI/CD) pipelines.

We acknowledge and celebrate the First Australians on whose traditional lands we meet, and pay our respects to the elders past, present and emerging. We especially pay our respects to the elders of the Ngunnawal people whose traditional lands include the ANU.