Skip to content

Latest commit

 

History

History
422 lines (347 loc) · 16.4 KB

papers.md

File metadata and controls

422 lines (347 loc) · 16.4 KB
Raw
layout title permalink
page
Papers, Talks and Patents
/papers/
  • Table of contents {:toc}

My Google Scholar, DBLP, ORCID and Microsoft Academic pages.

Papers

{% for paper in site.data.biblio %} {% endfor %}
{{ paper.ar_shortname | replace:' ',' '}} {{ paper.ar_title }}

Talks

Specifications

  • Goals of a modern ISA specification
    Programming Languages for Architecture (PLARCH)
    17 June, 2023
    [pdf]

    What should we consider when creating an ISA specification? What can we learn from the 1970s? What are the conflicts between different uses of an ISA specification?

    (Talking to other researchers after the workshop, it became clear that I had missed out something important: we need to have a range of tools available that can be adapted to suit various needs. If we don't, then people will continue to roll their own specialized spec because it is too hard to use the official one.)

  • Towards a formal specification of Intel’s x86 architecture
    Novel Architecture and Novel Design Automation (NANDA)
    Virtual.
    5--6 September, 2022
    [pdf]

    This talk is about my work on creating a formal specification of Intel's x86 architecture: goals, why it is easy, why it is hard and the research challenges I see in the future.

  • Leaky abstractions
    RISE summer school 2022
    Keynote talk
    UK Research Institute in Secure Hardware and Embedded Systems (RISE)
    Centre for Secure Information Technology (CSIT)
    Belfast UK
    20--21 July, 2022.
    [pdf]

    Since at least the 1950s, computer design has been viewed as a stack of separate concerns: programmers need not worry about how the hardware works as long as it satisfies its functional specification; and digital logic designers need not worry about how transistors work as long as they turn on and off. This separation has allowed engineers at each layer of the stack to innovate and has resulted in the remarkable improvements in power, performance and area seen over the last 70+ years. Layers in the stack can be changed independently of their neighbours because each layer in the stack only depends on an abstraction of the layer below. However, these abstractions are "leaky": the abstractions are approximate and they omit properties such as time, space and power. This talk is about the connections between leaky abstractions and security and on both recent research and research opportunities in relating architectural security to the hardware stack that it rests on.

  • Machine readable specifications at scale
    ZISC seminar, ETH Zurich
    Virtual
    2 June, 2022
    [pdf]

    There are lots of potential uses for machine readable specifications so you would think that every major real world artifact like long-lived hardware and software systems, protocols, languages, etc. would have a formal specification that is used by all teams extending, implementing, testing, verifying or securing the design. But, in practice, this is usually not true: most real world systems do not have a well tested, up to date, machine readable specification.

    This talk is about why you might want to change this and some things to consider as you go about it. In particular, it is about the use and creation of machine readable specifications at scale: when the number of engineers affected is counted in the thousands. This sort of scale leads to different problems and solutions than you would see in a 5–10 person project and both the challenges and the potential benefits are significantly larger.

    [See also my blog post [Machine readable specifications at scale]({{site.baseurl}}{% post_url 2022-01-25-mrs-at-scale %}).]

Rust Verification

Talks about the Rust verification project at Google.

  • How can we formally verify Rust for Linux
    Kangrejos (workshop attached to Linux Plumbers 2021).
    Virtual.
    13 September 2021. [pdf]

    This talk describes the state of formal verification for Rust code in the Linux kernel based on the [blog posts]({% post_url 2021-08-22-rust-on-linux-1 %}) I wrote.

  • Building Better Systems (Episode #11): Meeting Developers Where They Are
    23 July 2021 (recorded 2nd February). [youtube] [apple podcast] [simplecast] [mp3] [transcript]

    This 36 minute interview with Joey Dodds and Shpat Morina at Galois focuses on adoption and usability of verification tools and where we sit on the spectrum from high-assurance/high-cost to lower-assurance/lower-cost.

  • Using KLEE with Large Rust Programs
    KLEE workshop 2021
    Virtual (London, UK). 11 June 2021. [pdf] [video]

    This 12 minute talk focuses on tools: what we have done to adapt KLEE for use with Rust; the language, compiler, library and linker features we have encountered in real code out in the wild; and how we have tried to solve issues in a way that other Rust verification tools can directly use or adapt.

The Hardware-Software Interface: Quality and Performance

One of the most important interfaces in a computer system is the interface between hardware and software. This talk examines two critical aspects of defining the hardware-software interface: quality and performance.

The first aspect concerns the "radical" idea of creating a single, high-quality, formal specification of microprocessors that everybody can use. This idea does not seem "radical" until you realize that standard practice is for every group to create their own version of a specification in their preferred toolchain. I will describe the challenges that lead to this behavior and how to overcome the challenges. This project lead to the creation of Arm's official formal specification of their microprocessors and to the formal validation of Arm's processors against that specification.

The second aspect concerns the tradeoff between portability and performance in the context of high performance, energy efficient, parallel systems. I will describe the challenges in balancing portability and performance and how I overcame them by defining the hardware-software interface in terms of extensions of the C language. This project played a key part in creation of a software-defined radio system capable of implementing the 4G cellphone protocol.

The Arm architecture is the largest computer architecture by volume in the world; it behooves us to ensure that the interface it describes is appropriately defined.

  • Computer Science Department, Glasgow, UK. 21 February, 2019 [pdf]

Engineering and Using Large Formal Specifications

We have great tools and technique to formally verify hardware and software but, if we are apply these to real world systems, we need high quality specifications of real world artifacts such as processors, OSes, libraries, programming languages and internet protocols. This talk is about how we are going to avoid a specification bottleneck - it uses my experience in formalising the ARM processor architecture to suggest an approach that we can use on other large, complex hardware and software to create the specifications we need.

  • ACL2 2018
    Keynote talk, Austin, Texas, USA. 5-6 November, 2018. [pdf]

What makes processors fail - and how to prevent it

A more accessible presentation of the ideas in the ISA-Formal paper for the Electromagnetic Field maker festival.

Modern processors are amazing devices: small, fast, low power and getting better with every generation. But the most amazing things about modern microprocessors is that they work so incredibly reliably despite all their incredible complexity.

This talk is about the battle between complexity and correctness and about how new formal verification tools can be used to help you design higher performance processors that actually work. I will describe the common optimisations, the bugs that these often introduce and how open source tools such as SAT solvers and bounded model checkers can be used to find these bugs.

Creating Formal Specifications of the Arm Processor Architecture

A talk about why creating formal specifications for real world systems is hard and what we can do about it. Some of the key problems are the semantic gap between the architects’ intention and the written specification; challenges persuading different groups to adopt a common specification; the number and diversity of existing implementations; and the practical impossibility of formally verifying all implementations against the specification. I discuss lessons learned when creating a formal specification of the Arm Processor Architecture and using that specification to formally validate processors against the specification. And I discuss how those lessons can be applied in other contexts. This includes use of traditional testing, formal validation, social engineering and building a virtuous cycle to drive up the quality of the specification.

Specifications: The Next Verification Bottleneck

A talk about the importance and difficulty of creating trustworthy specifications of all the software and protocols we will need to verify software and about the techniques I used to create a trustworthy specification of the ARM processor architecture.

How can you trust formally verified software?

A talk about practical things you can do with ARM's executable formal specification with an emphasis on security research. Despite having the same title, this is a completely different talk from the next one. TUWAT!

How can you trust formally verified software?

A gradually evolving series of talks about my work on creating correct formal specifications (when there are multiple implementations already in existence). Reinforces the idea of having multiple users of a single specification and includes a short version of the FMCAD16, CAV16 and OOPSLA17 talks.

Trusting Large Specifications: The Virtuous Cycle

First talk emphasizing the importance of having multiple users of a single specification.

Trustworthy Specifications of ARM System Level Architecture

Backwards compatible formalization of the ARM Architecture

First public talk about creating formal specifications of ARM processors.

  • Cambridge University Computer Laboratory
    Cambridge, UK, February, 2012. [pdf]

Patents

{% for paper in site.data.patents %} {% endfor %}
{% if paper.link %} {{ paper.number | replace:' ',' '}} {% else %} {{ paper.number | replace:' ',' '}} {% endif %} {{ paper.title }}
{{ paper.author }}, {{ paper.location }} {{ paper.type }}, {{ paper.month }} {{ paper.year }}