A formal proof of the Chip Model Channel Separation Property

Thomas Hallgren, Talk at the Programatica Review Meeting, 2004-09-16

A formal proof of the Chip Model Channel Separation Property

Thomas Hallgren

Talk at the Programatica Review Meeting, 2004-09-16

   ┌─────────┐    ┌─────────┐
───┤ pick ch ├───►┤  chip   ├──►
   └─────────┘	  └─────────┘
=
   ┌─────────┐    ┌─────────┐
───┤  chip   ├───►┤ pick ch ├──►
   └─────────┘	  └─────────┘

The Chip

A model of a cryptographic chip, loosely based on the AIM chip from Motorola.

Proof of the separation property

The Chip Model in Haskell

chip :: [Packet] → [Packet] type Packet = (Channel,Data) type Channel = Int type Data = [Word]
      ┌──────┐
ps ───┤ chip ├──►  ps'
      └──────┘

Channel Separation Property in P-logic

Property of interest: channel separation ( = no information leaks between channels)
  ┌─────────┐   ┌─────────┐
──┤  chip   ├──►┤ pick ch ├──►
  └─────────┘   └─────────┘
=
  ┌─────────┐   ┌─────────┐
──┤ pick ch ├──►┤  chip   ├──►
  └─────────┘   └─────────┘
assert Separation = ∀ ch . {pick ch . chip} === {chip . pick ch} pick :: Channel → [Packet] → [Packet] pick ch = filter ((==ch).fst)

Alternative view of the Channel Separation Property

	┌──────┐
     ───┤ chip ├──►
        └──────┘
=
      ┌─────────┐   ┌─────────┐
   ┌─►┤ pick 1  ├──►┤  chip   ├──┐
   │  └─────────┘   └─────────┘  │
   │  ┌─────────┐   ┌─────────┐  │
───┼─►┤ pick 2  ├──►┤  chip   ├──┼──►
   │  └─────────┘   └─────────┘  │
   │      ...          ...       │
   │  ┌─────────┐   ┌─────────┐  │
   └─►┤ pick n  ├──►┤  chip   ├──┘
      └─────────┘   └─────────┘

Processing all channels in one chip is the same as having one chip per channel.

Filling in the details

This is the definition main Separation assertion:
chip :: Algs → ChipState → [Packet] → [Packet] type Algs = Channel → Alg type ChipState = (Memory,Regs) type Regs = FM RegFile assert Separation = ∀ algs . ∀ ch . ∀ state . ∀ ps . {pick ch (chip algs state ps)} === {chip algs state (pick ch ps)}

The Chip Model in Haskell, more details

chip :: Algs → ChipState → [Packet] → [Packet] chip algs state ps = fst (runS (manyPackets algs ps) state) manyPackets :: Algs → [Packet] → StateM ChipState [Packet] manyPackets algs = mapM (onePacket algs) onePacket :: Algs → Packet → StateM ChipState Packet onePacket algs (chan,ws) = do regfile ← liftM (\regs→FM.lookup regs chan) (inSnd load) (ws',regfile') ← inFst (doPacket (algs chan) ws regfile) finishPacket chan ws' regfile' doPacket :: Alg → Data → RegFile → StateM Memory (Data,RegFile) doPacket alg ws regf = ...

For reference...

Generic monadic operations

liftM :: Monad m ⇒ (a → b) → m a → m b mapM :: Monad m ⇒ (a → m b) → [a] → m [b]

State monad operations

inFst :: StateM s1 a → StateM (s1,s2) a inSnd :: StateM s2 a → StateM (s1,s2) a runS :: StateM s a → s → (a,s)

An observation

Although the function chip is defined in a monadic style, it is equivalent(*) to a simple list traversing function:
chip algs state [] = [] chip algs state (p:ps) = p':chip algs state' ps where (p',state') = runS (onePacket algs p) state

Under the assumption that onePacket has the right properties, we can prove Separation with induction over the input packet list, without reasoning about monadic code.

(*) This equivalence follows directly from the definitions.

Overall proof structure

The proof of Separation is obtained by combining two the proofs of two main properties: CondSeparation and AllGoodAlgs.
assert CondSeparation = ∀ algs ch state1 state2 ps . GoodAlg {algs ch} ==> Invariant state1 state2 ch ==> {pick ch (chip algs state1 ps)} === {chip algs state2 (pick ch ps)}
assert AllGoodAlg = ∀ alg . GoodAlg alg
This factoring of the proof as some advantages...

Observations

CondSeparation proof outline

AllGoodAlg proof outline

Proof effort

Proof size

Relevance to current work

The End

Questions?

References