Selected papers and talks

Rust support in seL4 userspace: Update and Roadmap
seL4 Summit 2023
Nick Spinale

The Supervisionary proof-checking kernel
Workshop on Principles of Secure Compilation (PriSC), POPL 2022
Dominic P. Mulligan and Nick Spinale

Confidential Computing—a brave new world
IEEE International Symposium on Secure and Private Execution Environment Design
Dominic P. Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell and Hugo J. M. Vincent

seL4 + TrustZone: Spanning both worlds
seL4 Summit 2020
Nick Spinale

Newly reducible polynomial iterates
International Journal of Number Theory
Peter Illig, Rafe Jones, Eli Orvis, Yukihiko Segawa, Nick Spinale

Selected open source activity

rust-sel4 - I have been working on seeding the seL4 userspace ecosystem with support for the Rust programming language. This work is funded by the seL4 Foundation.

IceCap - At Arm Research, I started and led the IceCap project. IceCap is a hypervisor with a minimal trusted computing base which serves as a research vehicle for virtualization-based confidential computing. The IceCap Framework, a byproduct of the IceCap Hypervisor, is a collection of tools and librarys for constructing seL4-based systems with CapDL and Rust.

seL4 - I am a contributor to seL4, the formally verified microkernel. My contributions span the kernel itself and CapDL.

Isabelle + Nix - The Isabelle developers suggested that trying to repackage, let alone port, Isabelle would be insane: [1] [2]. Nix provides a realistic and satisfying means to such a port. To prove it, I've used Nix to port Isabelle to Arm. This port has just recently become relevant due to the MacOS transition to Arm.

Nixpkgs - I am a contributor to the Nix packages collection.

Selected professional experience

Colias Group, LLC | Owner, Researcher, and Consultant
August 2022 – Present | Portland, OR

Arm Research | Senior Research Engineer
October 2018 – February 2022 | Cambridge, UK

Google | Software Engineering Intern
June – September 2017 | Mountain View, CA

Carve Systems, LLC | HackNY Fellow + Intern
June – December 2016 | New York, NY

Education

Carleton College | Mathematics and Computer Science
Sep 2014 – June 2018 | Northfield, MN

Honors

David Pollatsek Prize in Computer Science
2018 – Carleton College

Phi Beta Kappa
2018 – Carleton College

HackNY Fellow
2016 – hackNY

United States Presidential Scholar
2014 – United States Department of Education

Academic services

seL4 Summit 2024 | Program committee co-chair

Trusted Computing Center of Excellence Summit 2024 | Program committee

seL4 Summit 2023 | Program committee

seL4 Summit 2022 | Program committee

Arm Research Summit 2020 | Session chair
Morello: Investigating hardware capabilities in the Arm architecture – Richard Grisenthwaite (Chief Architect at Arm), Robert Watson (University of Cambridge), and Peter Sewell (University of Cambridge)

Selected independent projects

hs-arm - ARM (dis)assembler and analyzer Haskell library generated from the machine-readable ARMv8.3-A specification.

Malice - Haskell framework that provides abstractions and protocol-specific attacks for intercepting and modifying network traffic. It leverages the power of Haskell’s type system to define an embedded DSL for describing the actions of Eve and Mallory. In effect, it allows a person in the middle to write code that is as close to pure evil as possible.

pyxendbg - GDB server for virtual machine introspection under Xen. Inspired by xendbg, but with Arm in mind. Designed for debugging paravirtutalized unikernel guests.

regl - Haskell library for applicative-style regular expressions. Features uncommon yet useful primitives such as regular expression complement and disjunction. Based on regular expression derivatives.

kgo - kexec implemented in pure Go, with some extra flexibility. Designed to boot a type-1 hypervisor such as Xen or Hafnium, with LinuxBoot in mind.

routor - Tor controller that allows circuit paths to be chosen on a stream-by-stream basis.

wmonad - A set of Haskell libraries encapsulating interaction with the X11 server, enabling the expression of pure X11 logic.

Patents

US 17/076,112
Method and apparatus for encrypted communication
Gustavo Federico Petri, Guilhem Floreal Bryant, Nicholas Costas Spinale

GB2016674.0A
Methods and apparatus for communication between processing circuitry and a peripheral device
Gustavo Federico Petri, Guilhem Floréal Bryant, Nicholas Costas Spinale, Dominic Phillip Mulligan