slides.md

theme	class	highlighter	lineNumbers	drawings
apple-basic	text-center	prism	false	persist

provably
correct
software

is possible and necessary

how formal verification and Magmide could make
provably correct code tractable for practicing engineers

<style> .slidev-layout { @apply px-[7rem] pt-[1rem] text-left; } .slidev-layout h1 { @apply mb-[1rem]; font-size: 7rem; line-height: 1; } .slidev-layout h2 { @apply text-6xl mb-[2rem] font-light; } .slidev-layout h4 { @apply text-3xl; } </style>

---

Formal Verification

• What is it?
• Core ideas
• Magmide
• Prerequisites: type systems, especially Rust

---

Software is broken

• Security breaches
• Ransomware attacks
• Operational failures
• Safety critical failures

---

Software is broken

Consortium for Information & Software Quality

The Cost of Poor Software Quality in the US: A 2020 Report

• $1.56 trillion in operational failures
• $1.31 trillion in technical debt

McAfee

The Hidden Costs of Cybercrime

• $945 billion monetary loss from cybercrime in 2020
• $145 billion global spending on cybersecurity in 2020
• up from $522.5 billion in 2018

<style> .slidev-layout { @apply px-[10rem] py-[3rem] text-lg; } </style>

---

Software is broken

• Software underpins critical social infrastructure.
• Broken software hurts people.
• Broken software slows down human progress.

---

It doesn't have to be this way!

• Software is just information that represents pure logic.
• Relies on hardware assumptions, but can itself be literally mathematically perfect.
• Provably correct code is possible with formal verification.

---

Quanta Magazine: Hacker-Proof Code Confirmed

• DARPA funded team.
• Quadcopter control software.
• Red team of world-class hackers.
• Logical proof of security.
• Tools purpose-built by and for academics.

<style> .slidev-layout { @apply px-[12rem] py-[4rem] text-lg; } </style>

---

Magmide

• Bring formal verification out of the ivory tower to practicing engineers.
• Proof language as a verified bare metal program.
• Foundation for verified programs for any architecture or environment.

Is this possible?

• Understanding makes it easier to believe.

---

Core concepts of formal verification

• Dependent Types
• Type Checking is Proof Checking
• Separation Logic

---

Dependent Types

• More powerful than normal types.

---

fn is_one(n: u64) -> bool {
  n == 1
}

(u64) -> bool

<style> .slidev-layout { @apply text-3xl; } </style>

---

Same type as is_one, very different behaviors.

fn is_zero(n: u64) -> bool {
  n == 0
}
fn always_true(_: u64) -> bool {
  true
}
fn always_false(_: u64) -> bool {
  false
}
// ... many other possible functions

• Testing can only guarantee correctness with small finite functions.
• Real guarantees need the type system.

<style> .slidev-layout { @apply py-[2rem] text-xl; } </style>

---

Dependent Types

• Normal types can only reference other types.
• Dependent types can reference values.

---

Dependent Types (using Coq)

Program Definition is_one n: {b | b = true <-> n = 1} :=
  match n with
  | 1 => true
  | _ => false
  end.
Solve All Obligations with (simpl; lia).

forall (n: nat), {b: bool | b = true <-> n = 1}

Coq makes this painful, but it's possible!

---

Type Checking is Proof Checking

Program Definition is_one n: {b | b = true <-> n = 1} :=
  match n with
  | 0 => true // <- mistake!
  | _ => false
  end.
Solve All Obligations with (simpl; lia).
// ❌ unable to unify!

• The type system checks that everything is consistent.
• All type systems represent some logic.
• Type checkers basically find proofs.

---

Inductive Even: nat -> Prop :=
  | Even_0: Even 0
  | Even_plus_2: forall n, Even n -> Even (S (S n)).

• Even takes nat and gives logical proposition.
• Even_0 has type declaring 0 is even.
• Even_plus_2 has type that if any n is even, so is n + 2

---

Inductive Even: nat -> Prop :=
  | Even_0: Even 0
  | Even_plus_2: forall n, Even n -> Even (S (S n)).

Coq is lisp-like, not C-like.

• (foo a b) rather than foo(a, b).
• (S (S n)) same as n + 1 + 1.

---

Inductive Even: nat -> Prop :=
  | Even_0: Even 0
  | Even_plus_2: forall n, Even n -> Even (S (S n)).

Definition four_is_even: Even 4 :=
  (Even_plus_2 2 (Even_plus_2 0 Even_0)).

Definition four_is_even: Even 4.
Proof.
  repeat constructor.
Qed.

---

Fixpoint double (n: nat) :=
  match n with
  | O => O
  | S sub_n => S (S (double sub_n))
  end.

Definition even_double: forall n, Even (double n).
Proof.
  induction n; constructor; assumption.
Qed.

• even_double is a proof transforming function.
• even_double is literally infinitely better than a unit test.
• Didn't have to change definition of double.

<style> .slidev-layout { @apply py-[3rem]; } </style>

---

If you want to learn more:

• Software Foundations
• Certified Programming with Dependent Types
• and many others...

---

Dependently typed proof languages are extremely powerful:

• Feit–Thompson theorem
• DeepSpec
• HACMS: High Assurance Cyber Military Systems
• Project Everest

---

Why isn't everyone doing this?

• Research Debt
• Pure Functional Dogma

---

Research Debt - Chris Olah, Shan Carter

There's a tradeoff between the energy put into explaining an idea, and the energy needed to understand it. On one extreme, the explainer can painstakingly craft a beautiful explanation, leading their audience to understanding without even realizing it could have been difficult. On the other extreme, the explainer can do the absolute minimum and abandon their audience to struggle. This energy is called interpretive labor.

People expect the climb to be hard. It reflects the tremendous progress and cumulative effort that's gone into mathematics. The climb is seen as an intellectual pilgrimage, the labor a rite of passage. But the climb could be massively easier. It's entirely possible to build paths and staircases into these mountains. The climb isn't something to be proud of.

The climb isn't progress: the climb is a mountain of debt.

The insidious thing about research debt is that it's normal. Everyone takes it for granted, and doesn't realize that things could be different.

Academia has bad incentives to
properly explain and expose their work.

<style> .slidev-layout { @apply px-[6rem] pt-[4rem] pb-[5rem]; } </style>

---

Pure Functional Dogma

• No mutation or side effects.
• But it's always a lie!
• Computers are just big chunks of mutable state.
• Have to reason about real computation.

---

Separation Logic

• Logical framework for reasoning about mutable state.
• Can be defined and used within a pure logic like Coq.
• Surprisingly uncommon.

---

... Normal Logic

P ∧ Q

P ∧ Q
equivalent to:
(P ∧ Q) ∧ P

---

Perfectly reasonable for pure facts.

Even(4) ∧ (1 + 1 = 2)
equivalent to:
(Even(4) ∧ (1 + 1 = 2)) ∧ Even(4)

---

What about mutable facts?

a --> 1

memory location a points to 1

---

// {program assertions}

// {a --> 1}
let a_value = *a;
// {a --> 1}
assert(a_value == 1);
// {a --> 1}

// {a --> 1}
some_function(a);
// {a --> 1 ∧ a --> ???}
let a_value = *a;
assert(a_value == 1); // ❌

(a --> 1) ∧ (a --> 2)

<style> .slidev-layout { @apply py-[2rem]; } </style>

---

Normal Logic

• ∧ operator too lenient for mutable facts.
• Difficult to scale program reasoning.
• Had to reason about entire program rather than composable pieces.

---

Separation Logic

// Not Allowed! ❌
(a --> 1) * (a --> 1)

• pronounced "and separately"
• called separating conjunction
• requires state assertions to be disjoint, separate
• doesn't allow duplicating assertions

// Okay! ✅
(a --> 1) * (b --> 2)

---

// {a --> 1}
let a_value = *a;
assert(a_value == 1);
// {a --> 1}
some_function(a);
// {}
// let a_value = *a;
// ❌ no longer own a!

• Must give away ownership.
• Allows small-scale composable proofs.
• Directly inspired Rust.
• More concepts, can be more complex.

<style> .slidev-layout { @apply py-[3rem]; } </style>

---

Rust Borrow Checker

• Represents a decidable subset of a fractional separation logic.
• Like a "proof finder", sometimes called a certified decision procedure.
• Can always determine correctness of safe Rust.
• Can't figure out correctness of unsafe code.
• Rust needs unsafe to actually be realistic and useful.

<style> .slidev-layout { @apply py-[3rem]; } </style>

---

Iris Separation Logic

• Built to verify arbitrarily complex Rust programs.
• Written in Coq. Researchers write proofs rather than relying on a decidable algorithm.
• Iris from the ground up
• RustBelt: Securing the Foundations of the Rust Programming Language
• Type system, ownership and lifetimes, Send and Sync.
• Arc, Rc, Cell, RefCell, Mutex, RwLock, mem::swap, thread::spawn, rayon::join, take_mut
• Iris/Iron powerful enough to verify no resource leaks!

<style> .slidev-layout { @apply py-[3rem] text-xl; } </style>

---

Why isn't everyone using Iris?

• Research debt.
• Not a directly usable language.
• Not built into any other tools.
• Only built for "on the side" proofs.

funrec option_as_mut(x) ret ret :=
  let r = new(2) in
  letcont k() := delete(1, x); jump ret(r) in
  let y = ∗x in case ∗y of
  − r :=={inj 0} (); jump k()
  − r :=={inj 1} y.1; jump k()

---

Magmide

Necessities to achieve goal:

• Capable of arbitrary logic
• Capable of bare metal performance
• Gradually verifiable
• Fully reusable
• Practical and usable
• Taught effectively

---

Capable of arbitrary logic

• Max out logical power with full type theory.
• Able to formalize any assertion.
• Decidable subsets still possible.

---

Capable of bare metal performance

• Start at the lowest level, use Iris.
• Less performant abstractions still possible.
• LLVM-like abstract assembly language, hardware axioms at bottom.

<style> .slidev-layout { @apply py-[3rem] text-lg; } </style>

---

Gradually verifiable

• Trackable effects, for tracking safety and correctness conditions.
• Knowledge of program safety is absolute but flexible.
• Incremental adoption and realistic iteration.
• Converge toward correctness.

---

Fully reusable

• Verification pyramid.
• Foundations pass on provably safe abstractions.
• Metaprogramming and query-based compiler.
• Higher level languages can "lift" full power, have escape hatches, reuse Magmide compiler functions.
• Don't have to write proofs for everything.

---

Practical and usable

• Rust/Cargo prove we can have nice things.
• Remove incidental complexity, focus essential complexity.

---

Taught effectively

• This research needs to be applied.
• Respect user's time.
• Assume reader is trying to get something done.
• Concrete examples before formal definitions.
• Call out true prerequisites.
• Use graspable words not opaque and unsearchable non-ascii symbols.
• Syntax should make it easy to find definitions.

---

Magmide design

Separates pure Logic from computational Host.

                    represents and
                      implements
      +--------------------+--------------------+
      |                    |                    |
      |                    |                    |
      v                    |                    |
Logic Magmide              +-------------> Host Magmide
      |                                         ^
      |                                         |
      |                                         |
      +-----------------------------------------+
                    logically defines
                      and verifies

• C -> Rust
• Coq/LLVM -> Magmide
• Currently bootstrapping prototype
• Coq for initial proofs and LLVM for compilation

<style> .slidev-layout { @apply pl-[16rem] pr-[10rem] py-[2rem] text-xl; } .slidev-code, pre { @apply text-xs !important; } </style>

---

Widespread formal verification could bring us...

• Proof carrying code.
• Provably secure operating systems, firmware, network drivers, browsers, voting software...
• Safe package ecosystems.
• More advanced borrow checking algorithms.
• Approachable logic coach in many more hands.

---

This is achievable!

github.com/magmide/magmide

Thank you!