I work at Arm Research.
My interests include privacy, confidential computing, formal methods, trusted execution environments, operating systems, programming languages, and reverse engineering.
Please feel free to reach out using any of the links above.
Papers and talks
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
Isabelle + Nix - The Isabelle developers suggested that trying to repackage, let alone port, Isabelle would be insane:  . 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'm an active contributor to the Nix packages collection.
Selected professional experience
Arm Research | Senior Research Engineer
October 2018 – Present | Cambridge, UK
Google | Software Engineering Intern
June – September 2017 | Mountain View, CA
Carve Systems, LLC | HackNY Fellow + Intern
June – December 2016 | New York, NY
Carleton College | Mathematics and Computer Science
Sep 2014 – June 2018 | Northfield, MN
David Pollatsek Prize in Computer Science
2018 – Carleton College
Phi Beta Kappa
2018 – Carleton College
2016 – hackNY
United States Presidential Scholar
2014 – United States Department of Education
(Session chair) Morello: Investigating hardware capabilities in the Arm architecture
Arm Research Summit 2020 – 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.
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.
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.