From 8c7b75e744018a1fa108a40c993ade76475b2989 Mon Sep 17 00:00:00 2001 From: Kristina Date: Fri, 9 Oct 2026 23:43:19 +0200 Subject: [PATCH 1/8] Track in the core whether decode expects an instruction The core's Input carried an inputIsInstr flag telling decode whether the word on the bus was an instruction. The core already knows this: fetch reads the PC exactly when the memory stage does not use the bus, and the response arrives one cycle later. Record it in a new pipeline register, stateDeExpInstr, set by fetch and read by decode, and make Input a one-field newtype over the bus word. Simulate, HardwareSim, the memory service and Main no longer construct or report the flag. Alongside: - Output holds a plain Maybe (MemAccess f) combined with <|> (first access wins) instead of First, so readers drop getFirst. - withCtrlReset is inlined into pipe, and regWithFwd reads the control lines with a plain Maybe instead of MaybeT. - ISA.interp, dead since April 2025, is removed and interp' takes its name. - Instruction replaces isLoad/isStore with isMemInstr (the two were never used apart) and gains isEnvInstr, both previously defined in the proof. The isNop* helpers are removed; decode compares against the Nop reasons directly. - The low-level Leak/* models get the minimal changes needed to keep compiling. Co-Authored-By: Claude Opus 5.5 --- app/Main.hs | 3 +- src/Core.hs | 87 ++++++++++++++----------------- src/HardwareSim.hs | 13 +---- src/ISA.hs | 14 ++--- src/Instruction.hs | 39 ++++---------- src/Leak/MonitorPC/MonitorLeak.hs | 15 +++--- src/Leak/MonitorPC/PC.hs | 7 ++- src/Leak/PC/Leak.hs | 16 ++++-- src/Leak/PC/PC.hs | 5 +- src/Leak/SecretPC/PC.hs | 3 +- src/Simulate.hs | 20 +++---- 11 files changed, 91 insertions(+), 131 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 396e5a9..4b46a32 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -7,7 +7,6 @@ import Control.Monad (when, forM_) import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Core as Core import Data.Functor.Identity -import Data.Monoid (First (getFirst)) import Elf.ElfLoader import Data.Elf (Elf) import Elf.Syscall (handleSyscall, ProgramExitException(..)) @@ -76,12 +75,12 @@ instance Show LeakageDivergenceException where "-------------------------------", "", "Input:", - " inputIsInstr: " P.++ show (Core.inputIsInstr input), " inputMem: " P.++ show (Core.inputMem input), "", "State:", " PC (fetch): 0x" P.++ showHex (Core.stateFePc state) "", " PC (decode): 0x" P.++ showHex (Core.stateDePc state) "", + " Expects instruction (decode): " P.++ show (Core.stateDeExpInstr state), " PC (execute): 0x" P.++ showHex (Core.stateExPc state) "", " Instruction (execute): " P.++ show (Core.stateExInstr state), " Instruction (memory): " P.++ show (Core.stateMeInstr state), diff --git a/src/Core.hs b/src/Core.hs index 6bdf50d..b8e9462 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -3,13 +3,13 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DerivingStrategies #-} {-# OPTIONS_GHC -Wno-deriving-defaults #-} +{-# LANGUAGE InstanceSigs #-} {- HLINT ignore "Functor law" -} module Core ( initInput, init, initCtrl, - withCtrlReset, circuit, Input (..), Output (..), @@ -37,9 +37,7 @@ import Access import Clash.Prelude hiding (Ordering (..), Word, def, init, lift) import Control.Monad import Control.Monad.RWS -import Control.Monad.Trans.Maybe import Data.Maybe (fromMaybe, isJust) -import Data.Monoid import Instruction hiding (decode) import Memory.Types import RegFile @@ -57,12 +55,7 @@ topEntity :: topEntity = exposeClockResetEnable $ mealy (circuit @f @RegFile) (init @f @RegFile) -- | The input to the CPU. -data Input f = Input - { -- | Is this an instruction read? - inputIsInstr :: Bool, - -- | Reads from memory. - inputMem :: f Word - } +newtype Input f = Input {inputMem :: f Word} deriving instance (Show (f Word)) => Show (Input f) @@ -90,7 +83,7 @@ deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (MemAccess f) -- | The output of the CPU. newtype Output f = Output { -- | A memory access. - outMem :: First (MemAccess f) + outMem :: Maybe (MemAccess f) } deriving instance (Show (f Word)) => Show (Output f) @@ -100,11 +93,13 @@ deriving instance Generic (Output f) deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (Output f) instance Semigroup (Output f) where + (<>) :: Output f -> Output f -> Output f + -- When several stages access memory in one cycle, the first one wins. Output mem <> Output mem' = - Output (mem <> mem') + Output (mem <|> mem') instance Monoid (Output f) where - mempty = Output mempty + mempty = Output Nothing -- | CPU halt state data HaltState = EBreak Address | Syscall Address | SecurityViolation @@ -122,6 +117,8 @@ data StateG r f = State stateFePc :: Address, -- | Program counter decode stage. stateDePc :: Address, + -- | Does the decode stage expect an instruction? + stateDeExpInstr :: Bool, -- | Program counter execute stage. stateExPc :: Address, -- | Instruction execute stage. @@ -213,7 +210,9 @@ circuit = flip $ execRWS pipe -- | The CPU, composed of each stage. pipe :: (Access f, RegFileOps r) => CPUM r f () -pipe = void $ withCtrlReset $ do +pipe = do + -- The control lines need to be reset every tick. + modify $ \s -> s {stateCtrl = initCtrl} writeback memory execute @@ -221,17 +220,14 @@ pipe = void $ withCtrlReset $ do fetch initInput :: (Access f) => Input f -initInput = - Input - { inputIsInstr = False, - inputMem = pure 0 - } +initInput = Input (pure 0) init :: forall f r. (Access f, RegFileOps r) => StateG r f init = State { stateFePc = initPc, stateDePc = 0, + stateDeExpInstr = False, stateExPc = 0, stateExInstr = Nop FirstCycle, stateMeInstr = Nop FirstCycle, @@ -260,31 +256,24 @@ initCtrl = ctrlWbRegFwd = Nothing } --- | The control lines need to be reset every tick. -withCtrlReset :: CPUM r f () -> CPUM r f (Control f) -withCtrlReset m = do - modify $ \s -> s {stateCtrl = initCtrl} - m - gets stateCtrl - -- | Set security violation flag. setSecurityViolation :: CPUM r f () setSecurityViolation = modify $ \s -> s {stateHalt = Just SecurityViolation} --- | The fetch stage. +-- | Fetch stage. fetch :: CPUM r f () fetch = do pc <- gets stateFePc ctrl <- gets stateCtrl - -- Always try to read unless the instruction in the `memory` stage is a load or a store. - unless (ctrlMeMemInstr ctrl) $ - readPC pc - -- We stall if the instruction in the `memory` stage is a load or a store. let stall = ctrlMeMemInstr ctrl + -- Always try to read unless we stall. + unless stall $ + readPC pc + let next_pc = fromMaybe (fromMaybe @@ -298,7 +287,9 @@ fetch = do s { -- Increment program counter for next fetch. stateFePc = next_pc, -- Propagate program counter to next stage. - stateDePc = pc + stateDePc = pc, + -- Decode expects an instruction next cycle iff we fetch now. + stateDeExpInstr = not stall } -- | Decode stage. @@ -306,20 +297,21 @@ decode :: (Access f) => CPUM r f () decode = do input <- ask pc <- gets stateDePc + expInstr <- gets stateDeExpInstr ctrl <- gets stateCtrl - + ir <- - if inputIsInstr input + if expInstr then noSecrets' (inputMem input) (Nop Halted) (pure . decode') else pure $ Nop MemoryBusBusy - let halted = maybe False isNopHalted (ctrlExInstr ctrl) + let halted = ctrlExInstr ctrl == Just (Nop Halted) let call_current_cycle = maybe False isCall (ctrlExInstr ctrl) let break_current_cycle = maybe False isBreak (ctrlExInstr ctrl) - let jump_previous_cycle = maybe False isNopJumpFirstCycle (ctrlExInstr ctrl) - let store_hazard_previous_cycle = maybe False isNopStoreHazardFirstCycle (ctrlExInstr ctrl) - let load_hazard_previous_cycle = maybe False isNopLoadHazardFirstCycle (ctrlExInstr ctrl) + let jump_previous_cycle = ctrlExInstr ctrl == Just (Nop JumpFirstCycle) + let store_hazard_previous_cycle = ctrlExInstr ctrl == Just (Nop StoreHazardFirstCycle) + let load_hazard_previous_cycle = ctrlExInstr ctrl == Just (Nop LoadHazardFirstCycle) let jump_current_cycle = isJust (ctrlExJumpAddr ctrl) @@ -328,7 +320,7 @@ decode = do maybe False (storeHazard pc) (ctrlMeStoreAddrSize ctrl) let load_hazard_current_cycle = maybe False (loadHazard ir) (ctrlExInstr ctrl) - + let ir' -- Halt if the core is not running anymore. | halted = Nop Halted @@ -456,13 +448,12 @@ execute = do regWithFwd :: RegIdx -> f Word -> CPUM r f (f Word) regWithFwd idx def = do - let checkForFwd line = do - (fwdIdx, fwdVal) <- MaybeT $ gets $ line . stateCtrl + ctrl <- gets stateCtrl + let pick line = do + (fwdIdx, fwdVal) <- line ctrl guard $ fwdIdx == idx && idx /= 0 pure fwdVal - fmap (fromMaybe def) $ - runMaybeT $ - checkForFwd ctrlMeRegFwd <|> checkForFwd ctrlWbRegFwd + pure $ fromMaybe def (pick ctrlMeRegFwd <|> pick ctrlWbRegFwd) alu :: (Access f) => Arith -> f Word -> f Word -> f Word alu op lhs rhs = case op of @@ -477,7 +468,7 @@ alu op lhs rhs = case op of SLT -> set <$> ((<) <$> (sign <$> lhs) <*> (sign <$> rhs)) SLTU -> set <$> ((<) <$> lhs <*> rhs) where - shiftBits s = slice d4 d0 s + shiftBits = slice d4 d0 sign = unpack @(Signed 32) set b = if b then 1 else 0 @@ -525,6 +516,7 @@ branch op lhs rhs = case op of where sign = unpack @(Signed 32) +-- | Memory stage. memory :: CPUM r f () memory = do ir <- gets stateMeInstr @@ -556,12 +548,12 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} _ -> pure () --- | Commit computations to the register file. +-- | Writeback stage. writeback :: forall f r. (Access f, RegFileOps r) => CPUM r f () writeback = do input <- asks inputMem ir <- gets stateWbInstr - res <- gets stateWbRes + res <- gets stateWbRes case ir of Instruction.RType _ rd _ _ -> do @@ -589,8 +581,7 @@ writeback = do Instruction.IType (Env Break) _ _ _ -> do cont <- gets stateHaltNextPc modify $ \s -> s {stateHalt = Just (EBreak cont), stateHaltNextPc = 0} - _ -> do - setLines $ \c -> c {ctrlWbRegFwd = Nothing} + _ -> setLines $ \c -> c {ctrlWbRegFwd = Nothing} where writeRF :: RegIdx -> f Word -> CPUM r f () writeRF idx val = diff --git a/src/HardwareSim.hs b/src/HardwareSim.hs index 1adb0ef..fd56011 100644 --- a/src/HardwareSim.hs +++ b/src/HardwareSim.hs @@ -9,7 +9,6 @@ import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) import Core hiding (topEntity) import Data.Functor.Identity import Data.Maybe (fromMaybe) -import Data.Monoid import qualified GHC.TypeNats import Instruction hiding (decode) import RegFile @@ -33,16 +32,8 @@ system prog = cpuOut cpuInput :: Signal dom (Input Identity) cpuInput = register initInput input cpuOut = cpu @Identity cpuInput - ram = HardwareSim.mkRAM @Identity @PROG_SIZE @RAM_SIZE prog ((fromMaybe (MemAccess False 0 Word Nothing) . getFirst . outMem) <$> cpuOut) - input = - ( \o mread -> - Input - ( fromMaybe False $ memIsInstr <$> getFirst (outMem o) - ) - (Identity mread) - ) - <$> cpuOut - <*> ram + ram = HardwareSim.mkRAM @Identity @PROG_SIZE @RAM_SIZE prog (fromMaybe (MemAccess False 0 Word Nothing) . outMem <$> cpuOut) + input = Input . Identity <$> ram mkRAM :: forall f progSize ramSize dom. (Access f, HiddenClockResetEnable dom, KnownNat ((GHC.TypeNats.*) ramSize 4), KnownNat (progSize + ramSize), KnownNat ((GHC.TypeNats.*) (progSize + ramSize) 4)) => diff --git a/src/ISA.hs b/src/ISA.hs index 32caf9e..ead78c6 100644 --- a/src/ISA.hs +++ b/src/ISA.hs @@ -5,7 +5,7 @@ -- | The ISA specification: what each instruction means, and how the -- architectural state evolves. -- --- Two halves, both semantics. 'interp'' turns an 'Instruction.Instruction' into +-- Two halves, both semantics. 'interp' turns an 'Instruction.Instruction' into -- an @'Instr' 'Func'@ -- the effect it denotes -- and 'apply' evaluates one of -- those 'Func's against the two source-register values and the PC. On top of -- that, 'isaStep' says how the @(isaPc, isaRegFile, isaMem)@ triple moves. @@ -26,7 +26,6 @@ module ISA getR1, getR2, interp, - interp', IsaStateG (..), IsaState, StepG (..), @@ -119,13 +118,8 @@ instance DepReg (Instr Func) where deps Nop = (empty, empty) deps Syscall = (pure 17, empty) -interp :: (Access f) => Input f -> Instr Func -interp input - | not (inputIsInstr input) = Nop - | otherwise = interp' $ Instruction.decode' $ unAccess $ inputMem input - -interp' :: Instruction.Instruction -> Instr Func -interp' instr +interp :: Instruction.Instruction -> Instr Func +interp instr | Instruction.isBreak instr = Break | otherwise = case instr of @@ -259,7 +253,7 @@ isaStepDecoded ir st@(IsaState pc rf mem) = Break -> IsaHalted Syscall -> IsaHalted where - instr = interp' ir + instr = interp ir reg = maybe 0 (\idx -> runIdentity (lookupRFg idx rf)) diff --git a/src/Instruction.hs b/src/Instruction.hs index adb0a9a..69bf94f 100644 --- a/src/Instruction.hs +++ b/src/Instruction.hs @@ -20,15 +20,11 @@ module Instruction getRs2, isBreak, isCall, - isNopJumpFirstCycle, - isNopLoadHazardFirstCycle, - isNopStoreHazardFirstCycle, - isNopHalted, + isEnvInstr, break, storeHazard, loadHazard, - isLoad, - isStore, + isMemInstr, loadExtend, ) where @@ -442,29 +438,16 @@ isCall :: Instruction -> Bool isCall (IType (Env Call) _ _ _) = True isCall _ = False -isLoad :: Instruction -> Bool -isLoad (IType Load {} _ _ _) = True -isLoad _ = False +-- | @ecall@ / @ebreak@: the instructions that halt the core. +isEnvInstr :: Instruction -> Bool +isEnvInstr ir = isCall ir || isBreak ir -isStore :: Instruction -> Bool -isStore (SType {}) = True -isStore _ = False - -isNopJumpFirstCycle :: Instruction -> Bool -isNopJumpFirstCycle (Nop JumpFirstCycle) = True -isNopJumpFirstCycle _ = False - -isNopLoadHazardFirstCycle :: Instruction -> Bool -isNopLoadHazardFirstCycle (Nop LoadHazardFirstCycle) = True -isNopLoadHazardFirstCycle _ = False - -isNopStoreHazardFirstCycle :: Instruction -> Bool -isNopStoreHazardFirstCycle (Nop StoreHazardFirstCycle) = True -isNopStoreHazardFirstCycle _ = False - -isNopHalted :: Instruction -> Bool -isNopHalted (Nop Halted) = True -isNopHalted _ = False +-- | Loads and stores: the instructions that use the memory bus in the memory +-- stage. +isMemInstr :: Instruction -> Bool +isMemInstr (IType Load {} _ _ _) = True +isMemInstr (SType {}) = True +isMemInstr _ = False break :: Instruction break = IType (Env Break) 0 0 0 diff --git a/src/Leak/MonitorPC/MonitorLeak.hs b/src/Leak/MonitorPC/MonitorLeak.hs index c7569ab..1ca0f4d 100644 --- a/src/Leak/MonitorPC/MonitorLeak.hs +++ b/src/Leak/MonitorPC/MonitorLeak.hs @@ -30,7 +30,7 @@ data LeakMonitor si ii sl ol = LeakMonitor (sl1', o1) = f1 sl1 i (sl2', o2) = f2 sl2 i -monitorPC :: LeakMonitor (Core.State Identity) (Core.Input Identity) ((), Core.State Identity) (Instr, Maybe Address) +monitorPC :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity, Core.State Identity) (Instr, Maybe Address) monitorPC = monitorInstructionType ^&^ monitorJumpAddress data BaseInstr @@ -72,12 +72,15 @@ toLeakInstr input = Instr (mkInstr input) (getRs1' input) (getRs2' input) nop' :: Instr nop' = toLeakInstr nop -monitorInstructionType :: LeakMonitor (Core.State Identity) (Core.Input Identity) () Instr -monitorInstructionType = LeakMonitor (\() i -> ((), leak i)) (const ()) +monitorInstructionType :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity) Instr +monitorInstructionType = LeakMonitor leak id where - leak :: Core.Input Identity -> Instr - leak input | Core.inputIsInstr input = toLeakInstr $ decode' $ runIdentity $ Core.inputMem input - leak _ = nop' + leak :: Core.State Identity -> Core.Input Identity -> (Core.State Identity, Instr) + leak s i = (fst (Core.circuit s i), instr) + where + instr + | Core.stateDeExpInstr s = toLeakInstr $ decode' $ runIdentity $ Core.inputMem i + | otherwise = nop' monitorJumpAddress :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity) (Maybe Address) monitorJumpAddress = LeakMonitor leak id diff --git a/src/Leak/MonitorPC/PC.hs b/src/Leak/MonitorPC/PC.hs index 1b9a57f..bc05a26 100644 --- a/src/Leak/MonitorPC/PC.hs +++ b/src/Leak/MonitorPC/PC.hs @@ -18,7 +18,6 @@ import Core (Input (..), MemAccess (..), Output (..)) import qualified Core import Data.Functor.Identity import Data.Maybe (isJust, isNothing) -import Data.Monoid import qualified Leak.MonitorPC.MonitorLeak as Leak import qualified Leak.MonitorPC.Sim as Sim import Types @@ -32,14 +31,14 @@ obs = stateless obs' obs' :: Output Identity -> Maybe Address obs' o_sim = do - mem <- getFirst $ outMem o_sim + mem <- outMem o_sim guard $ memIsInstr mem pure $ memAddress mem -leak :: ((), Core.State Identity) -> Input Identity -> (((), Core.State Identity), (Leak.Instr, Maybe Address)) +leak :: (Core.State Identity, Core.State Identity) -> Input Identity -> ((Core.State Identity, Core.State Identity), (Leak.Instr, Maybe Address)) leak = Leak.leakCircuit Leak.monitorPC -proj :: Core.State Identity -> (((), Core.State Identity), Sim.State) +proj :: Core.State Identity -> ((Core.State Identity, Core.State Identity), Sim.State) proj s = (ts, ss) where ts = Leak.leakProject Leak.monitorPC s diff --git a/src/Leak/PC/Leak.hs b/src/Leak/PC/Leak.hs index 67130c7..1f8684b 100644 --- a/src/Leak/PC/Leak.hs +++ b/src/Leak/PC/Leak.hs @@ -68,6 +68,7 @@ nop = Instr (Nop Instr.FirstCycle) (Nothing, Nothing) data State = State { stateFePc :: Address, stateDePc :: Address, + stateDeExpInstr :: Bool, stateExPc :: Address, stateExInstr :: Instr.Instruction, stateMemInstr :: Instr.Instruction, @@ -92,6 +93,7 @@ init = State { stateFePc = initPc, stateDePc = 0, + stateDeExpInstr = False, stateExPc = 0, stateExInstr = Instr.Nop Instr.FirstCycle, stateMemInstr = Instr.Nop Instr.FirstCycle, @@ -157,14 +159,18 @@ fetch = do modify $ \s -> s { stateFePc = next_pc, - stateDePc = pc + stateDePc = pc, + -- The core fetches unless the memory stage uses the bus; a call does + -- not stop it. + stateDeExpInstr = not meMemInstr } decode :: LeakM () decode = do input <- ask + expInstr <- gets stateDeExpInstr let instr - | Core.inputIsInstr input = + | expInstr = Instr.decode' $ runIdentity $ Core.inputMem input | otherwise = Instr.Nop Instr.MemoryBusBusy @@ -175,9 +181,9 @@ decode = do mJumpAddr <- gets stateJumpAddr firstCycle <- gets stateFirstCycle - let branch_first_cycle = Instr.isNopJumpFirstCycle exInstr + let branch_first_cycle = exInstr == Instr.Nop Instr.JumpFirstCycle let load_hazard_current_cycle = Instr.loadHazard instr exInstr - let load_hazard_first_cycle = Instr.isNopLoadHazardFirstCycle exInstr + let load_hazard_first_cycle = exInstr == Instr.Nop Instr.LoadHazardFirstCycle let call_current_cycle = Instr.isCall exInstr let isSecretInstr = case fromPublic (Core.inputMem input) of Nothing -> True; _ -> False @@ -196,7 +202,7 @@ decode = do -- If this is the first cycle, the instruction to decode is gibberish from memory. else if firstCycle then Instr.Nop Instr.FirstCycle -- If memory is busy, we stall. - else if not (Core.inputIsInstr input) then Instr.Nop Instr.MemoryBusBusy + else if not expInstr then Instr.Nop Instr.MemoryBusBusy -- If we are in SecurityViolation state, we stall. else if isSecretInstr then Instr.Nop Instr.Halted -- Otherwise we process the decoded instruction. diff --git a/src/Leak/PC/PC.hs b/src/Leak/PC/PC.hs index 3ae2d3e..2e5cd6e 100644 --- a/src/Leak/PC/PC.hs +++ b/src/Leak/PC/PC.hs @@ -51,7 +51,7 @@ obs = stateless obs' obs' :: Output Identity -> Maybe Address obs' o_sim = do - mem <- getFirst $ outMem o_sim + mem <- outMem o_sim guard $ memIsInstr mem pure $ memAddress mem @@ -79,6 +79,7 @@ proj s = (ts, ss) Leak.State { Leak.stateFePc = Core.stateFePc s, Leak.stateDePc = Core.stateDePc s, + Leak.stateDeExpInstr = Core.stateDeExpInstr s, Leak.stateExPc = Core.stateExPc s, Leak.stateExInstr = Core.stateExInstr s, Leak.stateMemInstr = Core.stateMeInstr s, @@ -144,7 +145,7 @@ simulator = let (s_core', o_core) = implementation s_core_old i -- Update memory manually (register file is now in s_core') - let mem' = case getFirst (outMem o_core) of + let mem' = case outMem o_core of Just (MemAccess _ addr size (Just val)) -> mem {Simulate.memRAM = write size addr (runIdentity val) (Simulate.memRAM mem)} _ -> mem diff --git a/src/Leak/SecretPC/PC.hs b/src/Leak/SecretPC/PC.hs index fc68323..50ae8f7 100644 --- a/src/Leak/SecretPC/PC.hs +++ b/src/Leak/SecretPC/PC.hs @@ -24,7 +24,6 @@ import Core (Control (..), Input (..), MemAccess (..), Output (..), initInput) import qualified Core import Data.Bifunctor (second) import Data.Composition -import Data.Monoid (First (..), getFirst) import qualified Leak.Existence as Existence import qualified Leak.SecretPC.Leak as Leak import qualified Pantomime.Clash.NonInterference as P @@ -58,7 +57,7 @@ obs = stateless obs' obs' :: Output PubSec -> Maybe Address obs' o_sim = do - mem <- getFirst $ outMem o_sim + mem <- outMem o_sim guard $ memIsInstr mem pure $ memAddress mem diff --git a/src/Simulate.hs b/src/Simulate.hs index 887e4fa..aa0d314 100644 --- a/src/Simulate.hs +++ b/src/Simulate.hs @@ -21,7 +21,6 @@ import Core hiding (State) import qualified Core import Data.Functor.Identity import Data.Maybe (isJust) -import Data.Monoid import Memory.Types import Memory.Vec import Types @@ -42,28 +41,23 @@ simulator = where next :: Core.State f -> Output f -> m (Maybe (Input f)) next s (Output mem) = do - (mem_in, mem_instr) <- doMemory + mem_in <- doMemory if isJust (Core.stateHalt s) then pure Nothing - else pure $ - Just $ - Input - { inputIsInstr = mem_instr, - inputMem = mem_in - } + else pure (Just (Input mem_in)) where - doMemory :: m (f Word, Bool) + doMemory :: m (f Word) doMemory - | Just (MemAccess isInstr addr size mval) <- getFirst mem = + | Just (MemAccess isInstr addr size mval) <- mem = case mval of Nothing -> do word <- ramRead isInstr addr size isSecret <- isMemorySecret addr - pure (conditionalSecret isSecret word, isInstr) + pure (conditionalSecret isSecret word) Just val -> do ramWrite addr size (unAccess val) - pure (pure 0, isInstr) - | otherwise = pure (pure 0, False) + pure (pure 0) + | otherwise = pure (pure 0) runSimulator :: forall f ramSize progSize a. From 5a34df67dd95377dd7af15232f77c0dfb7047855 Mon Sep 17 00:00:00 2001 From: Kristina Date: Fri, 9 Oct 2026 23:43:38 +0200 Subject: [PATCH 2/8] Reorganise and simplify the functional proof Follow the core change: the invariant, driver and obligations read stateDeExpInstr where they read inputIsInstr, and the memory service in Proof.Machine no longer builds the flag. Layout: - Proof.Driver moves to Proof.Functional.Driver, next to the functional invariant and obligations. Proof.Machine stays shared: both proofs are about the system it defines. - The SMT helpers (Array, Axioms, Logged) move from proof/ to proof-smt/, so everything that talks to the solver lives behind the smt-proof flag. - KState and sysOf move from Proof.Functional.Induction into a new shared Proof.SMT.System (gaining the stateDeExpInstr field), so the functional and leakage inductions do not import each other and re-run each other's proofs on every change. - The notes under proof/notes are removed; the code comments now stand on their own. Simplifications: - isStartupShape and hopPc are removed: the base case already takes the initial state two cycles into the running case, and the tests use stateExPc directly. exInstr, isNopInstr and running go from Machine; callers read the state fields. - The base case is stated in Obligation as baseCaseObligation, for any start PC, register file and memory; Induction.baseCase instantiates it with symbolic values. indStep0 is renamed indStep. - The driver's exArg reads the register file as it stood at the start of the cycle plus the forwarding lines, without assuming writeback runs first; rfAfterWriteback goes. loadHazardD is renamed loadHazard and isJumpInstr takingJump. Co-Authored-By: Claude Opus 5.5 --- proof-smt/Proof/Functional/Induction.hs | 116 ++----------- {proof => proof-smt}/Proof/SMT/Array.hs | 0 {proof => proof-smt}/Proof/SMT/Axioms.hs | 0 {proof => proof-smt}/Proof/SMT/Logged.hs | 0 proof-smt/Proof/SMT/System.hs | 71 ++++++++ proof/Proof/{ => Functional}/Driver.hs | 125 ++++++-------- proof/Proof/Functional/Invariant.hs | 48 ++---- proof/Proof/Functional/Obligation.hs | 134 ++++++++------- proof/Proof/Machine.hs | 41 +---- proof/notes/counterexample-k0.txt | 143 ---------------- proof/notes/driver.txt | 91 ---------- proof/notes/invariant.txt | 206 ----------------------- proof/notes/leakage.txt | 53 ------ 13 files changed, 228 insertions(+), 800 deletions(-) rename {proof => proof-smt}/Proof/SMT/Array.hs (100%) rename {proof => proof-smt}/Proof/SMT/Axioms.hs (100%) rename {proof => proof-smt}/Proof/SMT/Logged.hs (100%) create mode 100644 proof-smt/Proof/SMT/System.hs rename proof/Proof/{ => Functional}/Driver.hs (64%) delete mode 100644 proof/notes/counterexample-k0.txt delete mode 100644 proof/notes/driver.txt delete mode 100644 proof/notes/invariant.txt delete mode 100644 proof/notes/leakage.txt diff --git a/proof-smt/Proof/Functional/Induction.hs b/proof-smt/Proof/Functional/Induction.hs index 1edaa2a..02c41a5 100644 --- a/proof-smt/Proof/Functional/Induction.hs +++ b/proof-smt/Proof/Functional/Induction.hs @@ -16,21 +16,13 @@ -- statements themselves live in "Proof.Functional.Obligation", shared with the QuickCheck -- harness so the two cannot drift. -- --- The pipeline state is passed as an ADT of scalars ('KState') plus SMT-array --- register file and memory: an ADT of scalars can be a fresh symbolic --- argument, a record containing a function cannot, and the Clash @Vec@ API is --- opaque to the plugin (see "Proof.SMT.Array"). +-- The pipeline state is passed as a 'KState' plus SMT-array register file and +-- memory; see "Proof.SMT.System". module Proof.Functional.Induction - ( -- | Exported because nothing in Haskell ever applies the constructor: the - -- plugin synthesises a 'KState' as a fresh symbolic input to each property, - -- and 'sysOf' only reads it back through the field accessors. Without this - -- the constructor looks dead to @-Wunused-top-binds@. It is also what a new - -- property in this module would take as its pipeline-state argument. - KState (..), - arrRoundTrip, + ( arrRoundTrip, shiftsSane, baseCase, - indStep0, + indStep, indStep1, indStep2, indStep3, @@ -38,64 +30,19 @@ module Proof.Functional.Induction ) where -import Proof.SMT.Array -import Proof.SMT.Axioms (arrayAxioms) import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import qualified Core import Data.Functor.Identity -import ISA (IsaStateG (..)) -import Instruction -import Proof.Functional.Invariant (invAtFree) -import Proof.SMT.Logged (pantomime) -import Proof.Machine -import Memory.Types (initPc) -import Proof.Driver (driver) -import Proof.Functional.Obligation import Pantomime (Theory (..)) import qualified Pantomime.BuiltIn as Pantomime +import Proof.Functional.Obligation +import Proof.SMT.Array +import Proof.SMT.Axioms (arrayAxioms) +import Proof.SMT.Logged (pantomime) +import Proof.SMT.System import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) --- | The pipeline registers, as plain scalars. -data KState = KState - { kFePc :: Address, - kDePc :: Address, - kExPc :: Address, - kExIr :: Instruction, - kMeIr :: Instruction, - kMeRes :: Word, - kMeAddr :: Address, - kWbIr :: Instruction, - kWbRes :: Word, - kCtrl :: Core.Control Identity, - kHalt :: Maybe Core.HaltState, - kHaltNextPc :: Address - } - --- | Assemble a system state from the symbolic pieces. -sysOf :: KState -> Core.Input Identity -> RegArr -> MemArr -> SysG RegArrF MemArr -sysOf ss i ra ma = - Sys - { sysState = - Core.State - { Core.stateFePc = kFePc ss, - Core.stateDePc = kDePc ss, - Core.stateExPc = kExPc ss, - Core.stateExInstr = kExIr ss, - Core.stateMeInstr = kMeIr ss, - Core.stateMeRes = Identity (kMeRes ss), - Core.stateMeAddr = kMeAddr ss, - Core.stateWbInstr = kWbIr ss, - Core.stateWbRes = Identity (kWbRes ss), - Core.stateRegFile = RegArrF ra, - Core.stateCtrl = kCtrl ss, - Core.stateHalt = kHalt ss, - Core.stateHaltNextPc = kHaltNextPc ss - }, - sysInput = i, - sysMem = ma - } - -- Sanity probes for the trusted embeddings ------------------------------------- -- -- The term axioms in "Proof.SMT.Axioms" replace Haskell functions by hand-written SMT @@ -126,48 +73,17 @@ shiftsSane x = -- The base case ---------------------------------------------------------------- --- | The invariant holds once the reset state has taken its first hop. --- --- Without this the four steps below say only that the invariant is /preserved/, --- which is vacuous if it never holds anywhere. Together they give the theorem: --- the invariant relates the core to the ISA at every state the driver lands on --- after reset. --- --- The reset state itself is not a case of the invariant. 'Core.init' has nothing --- in the pipeline, so the driver gives it a two-cycle hop that fetches and --- decodes the first instruction without executing anything. This property --- states that hop directly: the driver does assign it two cycles, and after --- them the running case relates the core to the ISA's /initial/ state -- zero --- ISA steps. Handling it here rather than as a case of the invariant is what --- lets every inductive step retire exactly one instruction. --- --- It holds for any loaded program, hence the arbitrary memory. Every field --- except the register file comes from 'Core.init' itself, so the reset shape --- cannot drift from the real one. The register file has to be substituted --- because 'RegFileOps.initRFg' builds a Clash 'Vec' with the opaque 'repeat'. --- --- Note what that substitution costs: memory and the register file are the same --- symbolic values on both sides, and the reset hop writes neither, so the --- invariant's two container equalities hold by construction here and this --- property alone would not notice if the core's reset register file and the --- ISA's ('RegFile.initRF') disagreed. The concrete test in "ProofSpec" closes --- that gap -- it runs on the real 'Vec'-backed state, where both files are built --- independently. {-# ANN baseCase (Theory arrayAxioms) #-} -baseCase :: RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -baseCase ra ma wr wa = - Pantomime.boolean $ driver sys == 1 && invAtFree wr wa isa (stepSys (stepSys sys)) - where - st = (Core.init :: Core.StateG RegArrF Identity) {Core.stateRegFile = RegArrF ra} - sys = Sys st Core.initInput ma - isa = IsaState {isaPc = initPc, isaRegFile = RegArrF ra, isaMem = ma} +baseCase :: RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool +baseCase ra ma wr wa pc = + Pantomime.boolean $ baseCaseObligation (RegArrF ra) ma wr wa pc -- The inductive steps ---------------------------------------------------------- -- | @k = 0@: the one-cycle hop (steady, writeback non-memory). -{-# ANN indStep0 (Theory arrayAxioms) #-} -indStep0 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -indStep0 ss i ra ma wr wa ipc = +{-# ANN indStep (Theory arrayAxioms) #-} +indStep :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool +indStep ss i ra ma wr wa ipc = Pantomime.boolean $ indStepObligation wr wa ipc (sysOf ss i ra ma) -- | @k = 1@: the two-cycle hop (a memory instruction in writeback). @@ -196,7 +112,7 @@ results = [ ("arrRoundTrip", $(pantomime 'arrRoundTrip)), ("shiftsSane", $(pantomime 'shiftsSane)), ("baseCase", $(pantomime 'baseCase)), - ("indStep0", $(pantomime 'indStep0)), + ("indStep", $(pantomime 'indStep)), ("indStep1", $(pantomime 'indStep1)), ("indStep2", $(pantomime 'indStep2)), ("indStep3", $(pantomime 'indStep3)) diff --git a/proof/Proof/SMT/Array.hs b/proof-smt/Proof/SMT/Array.hs similarity index 100% rename from proof/Proof/SMT/Array.hs rename to proof-smt/Proof/SMT/Array.hs diff --git a/proof/Proof/SMT/Axioms.hs b/proof-smt/Proof/SMT/Axioms.hs similarity index 100% rename from proof/Proof/SMT/Axioms.hs rename to proof-smt/Proof/SMT/Axioms.hs diff --git a/proof/Proof/SMT/Logged.hs b/proof-smt/Proof/SMT/Logged.hs similarity index 100% rename from proof/Proof/SMT/Logged.hs rename to proof-smt/Proof/SMT/Logged.hs diff --git a/proof-smt/Proof/SMT/System.hs b/proof-smt/Proof/SMT/System.hs new file mode 100644 index 0000000..69e9f4a --- /dev/null +++ b/proof-smt/Proof/SMT/System.hs @@ -0,0 +1,71 @@ +-- | The system state in a form the solver can take as a fresh symbolic input. +-- +-- The pipeline registers are passed as an ADT of scalars ('KState'), and the +-- register file and memory as SMT arrays: an ADT of scalars can be a fresh +-- symbolic argument, a record containing a function cannot, and the Clash +-- @Vec@ API is opaque to the plugin (see "Proof.SMT.Array"). 'sysOf' assembles +-- the pieces into a 'Proof.Machine.SysG'. +-- +-- Shared by the functional and the leakage inductions, so that neither imports +-- the other: their obligations are discharged while GHC compiles them, and an +-- import between them would re-run one proof whenever the other changes. +module Proof.SMT.System + ( -- | Exported because nothing in Haskell ever applies the constructor: the + -- plugin synthesises a 'KState' as a fresh symbolic input to each property, + -- and 'sysOf' only reads it back through the field accessors. Without this + -- the constructor looks dead to @-Wunused-top-binds@. + KState (..), + sysOf, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import qualified Core +import Data.Functor.Identity +import Instruction (Instruction) +import Proof.Machine +import Proof.SMT.Array +import Types +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | The pipeline registers, as plain scalars. +data KState = KState + { kFePc :: Address, + kDePc :: Address, + kDeExpInstr :: Bool, + kExPc :: Address, + kExIr :: Instruction, + kMeIr :: Instruction, + kMeRes :: Word, + kMeAddr :: Address, + kWbIr :: Instruction, + kWbRes :: Word, + kCtrl :: Core.Control Identity, + kHalt :: Maybe Core.HaltState, + kHaltNextPc :: Address + } + +-- | Assemble a system state from the symbolic pieces. +sysOf :: KState -> Core.Input Identity -> RegArr -> MemArr -> SysG RegArrF MemArr +sysOf ss i ra ma = + Sys + { sysState = + Core.State + { Core.stateFePc = kFePc ss, + Core.stateDePc = kDePc ss, + Core.stateDeExpInstr = kDeExpInstr ss, + Core.stateExPc = kExPc ss, + Core.stateExInstr = kExIr ss, + Core.stateMeInstr = kMeIr ss, + Core.stateMeRes = Identity (kMeRes ss), + Core.stateMeAddr = kMeAddr ss, + Core.stateWbInstr = kWbIr ss, + Core.stateWbRes = Identity (kWbRes ss), + Core.stateRegFile = RegArrF ra, + Core.stateCtrl = kCtrl ss, + Core.stateHalt = kHalt ss, + Core.stateHaltNextPc = kHaltNextPc ss + }, + sysInput = i, + sysMem = ma + } diff --git a/proof/Proof/Driver.hs b/proof/Proof/Functional/Driver.hs similarity index 64% rename from proof/Proof/Driver.hs rename to proof/Proof/Functional/Driver.hs index 5b7117b..261a2a5 100644 --- a/proof/Proof/Driver.hs +++ b/proof/Proof/Functional/Driver.hs @@ -1,40 +1,34 @@ --- | The driver from @proof/notes/driver.txt@, as code. --- --- The driver says how many cycles 'Proof.Machine.stepSys' should advance the core +-- | The driver: how many cycles 'Proof.Machine.stepSys' should advance the core -- before its state is compared against the ISA again. Its stated invariant is -- operational -- \"step until the instruction in the execute phase is no longer -- a no-op\" -- so this module provides both: -- --- * 'driver', the case table from @driver.txt@, and +-- * 'driver', a case table over the pipeline state, and -- * 'driverRef', the operational reading, obtained by actually stepping. -- -- Checking these two against each other is the first thing the test suite does. -- --- NOTE on signatures: @driver.txt@ writes @isJumpInstr@ and @storeHazard@ as --- functions of a handful of state fields. They cannot in fact be computed from --- those fields alone -- both depend on the execute stage's forwarded operand +-- 'takingJump' and 'storeHazard' are functions of the whole system state rather +-- than of a few fields: both depend on the execute stage's forwarded operand -- values, which in turn depend on the register file, on the memory-stage and -- writeback-stage forwarding lines, and (for a load in writeback) on --- 'inputMem'. So they are given here as functions of the whole system state. --- The stage ordering below mirrors 'Core.pipe': writeback, then memory, then --- execute. -module Proof.Driver +-- 'inputMem'. +module Proof.Functional.Driver ( driver, driverCaseName, driverRef, - isMemInstr, - isEnvInstr, - isJumpInstr, + takingJump, storeHazard, - loadHazardD, + loadHazard, exArg, + isBubble ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core import Data.Functor.Identity -import Instruction hiding (storeHazard) +import Instruction hiding (loadHazard, storeHazard) import qualified Instruction import Memory.Types (MemOps (..)) import Proof.Machine @@ -42,30 +36,6 @@ import RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) --- | From @invariant.txt@: loads and stores are the memory instructions. -isMemInstr :: Instruction -> Bool -isMemInstr ir = isLoad ir || isStore ir - --- | @ecall@ / @ebreak@. -isEnvInstr :: Instruction -> Bool -isEnvInstr ir = isCall ir || isBreak ir - --- | The register file as 'Core.execute' sees it, i.e. after 'Core.writeback' --- has committed the writeback-stage instruction. -rfAfterWriteback :: (RegFileOps r) => SysG r m -> r Identity -rfAfterWriteback (Sys st inp _) = - case stateWbInstr st of - RType _ rd _ _ -> put rd res - IType (Arith _) rd _ _ -> put rd res - IType (Load size sign) rd _ _ -> put rd (pure (loadExtend size sign (runIdentity (inputMem inp)))) - JType rd _ -> put rd res - IType Jump rd _ _ -> put rd res - UType _ rd _ -> put rd res - _ -> stateRegFile st - where - res = stateWbRes st - put rd v = modifyRFg rd v (stateRegFile st) - -- | @ctrlMeRegFwd@ as set by 'Core.memory'. Note that a load in the memory -- stage forwards nothing (its value is not available yet). meFwd :: SysG r m -> Maybe (RegIdx, Word) @@ -98,10 +68,10 @@ wbFwd (Sys st inp _) = -- | The value 'Core.execute' reads for a source register, honouring the -- memory-then-writeback forwarding priority of 'Core.execute'. exArg :: (RegFileOps r) => SysG r m -> RegIdx -> Word -exArg sys idx = +exArg sys@(Sys st _ _) idx = case pick (meFwd sys) <|> pick (wbFwd sys) of Just v -> v - Nothing -> runIdentity (lookupRFg idx (rfAfterWriteback sys)) + Nothing -> runIdentity (lookupRFg idx (stateRegFile st)) where pick m = do (fwdIdx, fwdVal) <- m @@ -109,9 +79,9 @@ exArg sys idx = -- | Does the execute-stage instruction take a jump this cycle? This is -- @ctrlExJumpAddr@ becoming 'Just'. -isJumpInstr :: (RegFileOps r) => SysG r m -> Bool -isJumpInstr sys = - case exInstr sys of +takingJump :: (RegFileOps r) => SysG r m -> Bool +takingJump sys@(Sys st _ _) = + case stateExInstr st of BType cmp _ rs1 rs2 -> runIdentity (branch cmp (pure (exArg sys rs1)) (pure (exArg sys rs2))) JType _ _ -> True @@ -134,7 +104,7 @@ storeHazard sys@(Sys st _ _) = || maybe False (Instruction.storeHazard dePc) meStore where dePc = stateDePc st - exStore = case exInstr sys of + exStore = case stateExInstr st of SType size imm rs1 _ -> Just ( unpack (runIdentity (alu ADD (pure (exArg sys rs1)) (pure (signExtend imm)))), @@ -147,48 +117,55 @@ storeHazard sys@(Sys st _ _) = -- | The load-hazard condition of 'Core.decode', between the instruction -- arriving on 'inputMem' and the one in the execute stage. -loadHazardD :: SysG r m -> Bool -loadHazardD sys@(Sys _ inp _) = - Instruction.loadHazard deIr (exInstr sys) +loadHazard :: SysG r m -> Bool +loadHazard (Sys st inp _) = + Instruction.loadHazard deIr (stateExInstr st) where + expInstr = stateDeExpInstr st deIr - | inputIsInstr inp = decode' (runIdentity (inputMem inp)) + | expInstr = decode' (runIdentity (inputMem inp)) | otherwise = Nop MemoryBusBusy --- | The case table from @driver.txt@, in order. +-- | The driver's case table. The cases are checked in order. driver :: (RegFileOps r) => SysG r m -> Int driver sys@(Sys st _ _) - | ex == Nop FirstCycle = 1 - -- @driver.txt@ has no case for a halted core; every other case is guarded by - -- @stateHalt == Running@. - | not (running sys) = 0 - | isEnvInstr ex = 2 - | isJumpInstr sys = 2 - | storeHazard sys = if isMemInstr ex then 3 else 2 - | loadHazardD sys = 3 + | stateExInstr st == Nop FirstCycle = 1 + | stateExInstr st == Nop Halted = 0 + | isEnvInstr (stateExInstr st) = 2 + | takingJump sys = 2 + | storeHazard sys = if isMemInstr (stateExInstr st) then 3 else 2 + | loadHazard sys = 3 | not (isMemInstr (stateWbInstr st)) = 0 | not (isMemInstr (stateMeInstr st)) = 1 - | not (isMemInstr ex) = 2 + | not (isMemInstr (stateExInstr st)) = 2 | otherwise = 3 - where - ex = exInstr sys -- | Which case of the table 'driver' fired. Used to measure how much of the -- table the tests actually reach. driverCaseName :: (RegFileOps r) => SysG r m -> String driverCaseName sys@(Sys st _ _) - | ex == Nop FirstCycle = "firstCycle" - | not (running sys) = "halted" - | isEnvInstr ex = "env" - | isJumpInstr sys = "jump" - | storeHazard sys = if isMemInstr ex then "storeHazard/mem" else "storeHazard/nomem" - | loadHazardD sys = "loadHazard" + | stateExInstr st == Nop FirstCycle = "firstCycle" + | stateExInstr st == Nop Halted = "halted" + | isEnvInstr (stateExInstr st) = "env" + | takingJump sys = "jump" + | storeHazard sys = if isMemInstr (stateExInstr st) then "storeHazard/mem" else "storeHazard/nomem" + | loadHazard sys = "loadHazard" | not (isMemInstr (stateWbInstr st)) = "steady/wb-nomem" | not (isMemInstr (stateMeInstr st)) = "steady/me-nomem" - | not (isMemInstr ex) = "steady/ex-nomem" + | not (isMemInstr (stateExInstr st)) = "steady/ex-nomem" | otherwise = "steady/all-mem" - where - ex = exInstr sys + +-- | Is this a pipeline bubble, as opposed to a real instruction? +-- +-- The driver's stated invariant is \"step until the execute stage is no longer +-- a no-op\", but that is slightly too coarse: @Nop DecodeFail@ is what an +-- undecodable memory word decodes to, so it /is/ the architectural instruction +-- at that PC and the ISA steps over it like any other. Only the stall reasons +-- are genuine bubbles. +isBubble :: Instruction -> Bool +isBubble (Nop DecodeFail) = False +isBubble (Nop _) = True +isBubble _ = False -- | The operational reading of the driver's stated invariant: step until the -- execute stage holds something that is not a no-op. Returns the number of @@ -196,13 +173,13 @@ driverCaseName sys@(Sys st _ _) -- happens once the core has halted, since the execute stage then holds -- @Nop Halted@ forever). -- --- \"No longer a no-op\" is read as 'Proof.Machine.isBubble': @Nop DecodeFail@ counts +-- \"No longer a no-op\" is read as 'isBubble': @Nop DecodeFail@ counts -- as a real instruction, since it is what an undecodable word in memory -- decodes to. driverRef :: (RegFileOps r, MemOps m) => Int -> SysG r m -> Maybe Int driverRef fuel sys0 = go 1 (stepSys sys0) where - go n s - | not (isBubble (exInstr s)) = Just n + go n s@(Sys st _ _) + | not (isBubble (stateExInstr st)) = Just n | n >= fuel = Nothing | otherwise = go (n + 1) (stepSys s) diff --git a/proof/Proof/Functional/Invariant.hs b/proof/Proof/Functional/Invariant.hs index 4cfe520..c496d35 100644 --- a/proof/Proof/Functional/Invariant.hs +++ b/proof/Proof/Functional/Invariant.hs @@ -1,8 +1,9 @@ --- | The invariant from @proof/notes/invariant.txt@, as code. +{- HLINT ignore "Use isNothing" -} +-- | The functional-correctness invariant. -- -- The invariant relates an architectural state @(isaPc, isaRegFile, isaMem)@ to -- a system state @((core state), (input), mem)@. It is a disjunction of cases: --- four for the running core, and two for the halted core. The reset state is +-- one for the running core, and two for the halted core. The reset state is -- not among them: 'Proof.Functional.Induction.baseCase' steps it two cycles, -- into the running case, instead. -- @@ -17,18 +18,6 @@ -- -- The test \"fold-free invariant agrees with the list version\" keeps the two -- from drifting. --- --- == Where this differs from @invariant.txt@ --- --- One place, marked again at its definition: NO @stateCtrl == initCtrl@ clause. --- It is a holdover from an earlier 'Core' that reset the control lines at the --- /end/ of each clock cycle; 'Core.withCtrlReset' now resets them at the start, --- so no state reached by stepping the core satisfies it. --- --- The note's four running cases are collapsed into one here. They differ only --- in the fetch conjuncts, and those track the writeback stage alone; the memory --- stage's classification does no work beyond excluding an environment --- instruction. See 'invCasesGen'. module Proof.Functional.Invariant ( flushWbStage, flushMeStage, @@ -47,7 +36,6 @@ import Core import Data.Functor.Identity import Instruction import Memory.Types -import Proof.Driver (isEnvInstr, isMemInstr) import ISA (IsaStateG (..), IsaState) import Proof.Machine import RegFile @@ -154,17 +142,9 @@ invCasesAt wr wa = -- | The cases of the invariant, parameterised over how register files and -- memories are compared. -- --- The one deviation from @invariant.txt@ is a silence: the note opens every --- case with @stateCtrl == initCtrl@, and no case here has it. That clause dates from an --- earlier 'Core' which reset the control lines at the end of each clock cycle, --- leaving them at their reset values by the time the next cycle began. --- 'Core.withCtrlReset' now resets them at the /start/ of the cycle and the --- stages then set them, so the lines observed in any post-step state are the --- ones the stages left -- 'Core.execute' alone always sets @ctrlExInstr@ to --- 'Just'. Only 'Core.init' still satisfies the clause, so keeping it would make --- the invariant hold of no state the driver lands on and every obligation --- vacuous. Dropping it is sound because the lines carry no information between --- cycles: 'Core.withCtrlReset' overwrites them before any stage reads them. +-- No case constrains @stateCtrl@. The control lines carry no information between +-- cycles: 'Core.pipe' resets them at the start of each cycle, before any stage +-- reads them. invCasesGen :: (RegFileOps r, MemOps m) => (r Identity -> r Identity -> Bool) -> @@ -172,7 +152,7 @@ invCasesGen :: IsaStateG r m -> SysG r m -> [Case] -invCasesGen eqRF eqMem (IsaState ipc irf imem) sys@(Sys st inp mem) = +invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys st inp mem) = [ runningCase, haltedCase "halted/ebreak" isBreak (EBreak (ipc + 4)), haltedCase "halted/ecall" isCall (Syscall (ipc + 4)) @@ -198,7 +178,7 @@ invCasesGen eqRF eqMem (IsaState ipc irf imem) sys@(Sys st inp mem) = -- therefore stated directly as \"not an environment instruction\". runningCase = Case "running" $ - [ ("running", running sys), + [ ("running", stateHalt st == Nothing), ("wb is not an env instruction", P.not (isEnvInstr (stateWbInstr st))), ("me is not an env instruction", P.not (isEnvInstr (stateMeInstr st))), ("exPc == isaPc", stateExPc st == ipc), @@ -217,11 +197,11 @@ invCasesGen eqRF eqMem (IsaState ipc irf imem) sys@(Sys st inp mem) = ] P.++ if isMemInstr (stateWbInstr st) then - [ ("not inputIsInstr", P.not (inputIsInstr inp)), + [ ("not deExpInstr", P.not (stateDeExpInstr st)), ("fePc == exPc + 4", stateFePc st == stateExPc st + 4) ] else - [ ("inputIsInstr", inputIsInstr inp), + [ ("deExpInstr", stateDeExpInstr st), ("inputMem == mem[dePc]", inputWord == dePcWord), ("fePc == exPc + 8", stateFePc st == stateExPc st + 8) ] @@ -266,8 +246,8 @@ data HaltKind = HaltBreak | HaltCall runningCaseAt :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool -runningCaseAt wr wa (IsaState ipc irf imem) sys@(Sys st inp mem) = - running sys +runningCaseAt wr wa (IsaState ipc irf imem) (Sys st inp mem) = + stateHalt st == Nothing && not (isEnvInstr (stateWbInstr st)) && not (isEnvInstr (stateMeInstr st)) && stateExPc st == ipc @@ -275,9 +255,9 @@ runningCaseAt wr wa (IsaState ipc irf imem) sys@(Sys st inp mem) = && stateDePc st == stateExPc st + 4 && not (loadHazard (stateExInstr st) (stateMeInstr st)) && ( if isMemInstr (stateWbInstr st) - then not (inputIsInstr inp) && stateFePc st == stateExPc st + 4 + then not (stateDeExpInstr st) && stateFePc st == stateExPc st + 4 else - inputIsInstr inp + stateDeExpInstr st && runIdentity (inputMem inp) == memReadWord (stateDePc st) mem && stateFePc st == stateExPc st + 8 ) diff --git a/proof/Proof/Functional/Obligation.hs b/proof/Proof/Functional/Obligation.hs index 195960a..9fcb0e5 100644 --- a/proof/Proof/Functional/Obligation.hs +++ b/proof/Proof/Functional/Obligation.hs @@ -7,8 +7,7 @@ -- input space, not the property. module Proof.Functional.Obligation ( isaAt, - hopPc, - isStartupShape, + baseCaseObligation, indStepObligation, indStepObligation1, indStepObligation2, @@ -19,9 +18,8 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import qualified Core import Data.Functor.Identity -import Proof.Driver (driver) +import Proof.Functional.Driver (driver) import ISA (IsaStateG (..), StepG (..), isaStep) -import Instruction import Proof.Functional.Invariant import Memory.Types (MemOps (..)) import Proof.Machine @@ -44,9 +42,8 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- -- @isaPc@ is different, and is quantified rather than derived. It is a scalar, -- so the invariant pins it exactly -- but via a different conjunct in each case: --- @stateExPc@ when running, @stateFePc@ at startup, and @stateHalt@ once halted. --- Deriving it from any one of those would make the other two cases --- unsatisfiable as premises. +-- @stateExPc@ when running and @stateHalt@ once halted. Deriving it from either +-- one would make the other case unsatisfiable as a premise. isaAt :: (RegFileOps r, MemOps m) => Address -> SysG r m -> IsaStateG r m isaAt ipc (Sys st inp mem) = IsaState {isaPc = ipc, isaRegFile = frf, isaMem = fm} @@ -63,36 +60,47 @@ isaAt ipc (Sys st inp mem) = (mem, Core.stateRegFile st) ) --- | Does the pipeline have the reset shape: nothing in flight, nothing on the bus? +-- | The base case: the invariant holds once the initial state has taken its +-- first hop. -- --- Not a case of the invariant -- 'Proof.Functional.Induction.baseCase' takes the --- reset state two cycles into the running case -- so no obligation needs it. It --- is kept for 'hopPc' and the leakage projection, which still assign an --- architectural state to the reset shape. -isStartupShape :: SysG r m -> Bool -isStartupShape (Sys st inp _) = - Core.stateWbInstr st == Nop FirstCycle - && Core.stateMeInstr st == Nop FirstCycle - && Core.stateExInstr st == Nop FirstCycle - && not (Core.inputIsInstr inp) - --- | The architectural PC a hop-aligned state corresponds to. +-- Without this the four steps below say only that the invariant is /preserved/, +-- which is vacuous if it never holds anywhere. Together they give the theorem: +-- the invariant relates the core to the ISA at every state the driver lands on +-- after the start. -- --- The symbolic obligations do not use this -- they quantify @isaPc@ and let the --- invariant pin it, which is the whole point of quantifying rather than --- deriving. It exists for the callers that need a concrete architectural state --- rather than a quantified one: the QuickCheck harness and the leakage --- projection. It reproduces, per case, the conjunct that pins @isaPc@ in the --- invariant -- the trapping instruction once halted, the execute stage --- otherwise -- plus the fetch stage for the reset shape, which the invariant does --- not admit but the leakage projection still assigns a PC. -hopPc :: SysG r m -> Address -hopPc sys@(Sys st _ _) - | isStartupShape sys = Core.stateFePc st - | otherwise = case Core.stateHalt st of - Just (Core.EBreak a) -> a - 4 - Just (Core.Syscall a) -> a - 4 - _ -> Core.stateExPc st +-- The initial state itself is not a case of the invariant. 'Core.init' has +-- nothing in the pipeline, so the driver gives it a two-cycle hop that fetches +-- and decodes the first instruction without executing anything. This property +-- states that hop directly: the driver does assign it two cycles, and after +-- them the running case relates the core to the ISA's /initial/ state -- zero +-- ISA steps. Handling it here rather than as a case of the invariant is what +-- lets every inductive step retire exactly one instruction. +-- +-- The start PC, the register file and memory are parameters, used for both the +-- core and the ISA; every other field comes from 'Core.init' itself, so the +-- initial pipeline shape cannot drift from the real one. Taking them as +-- parameters makes the base case cover any loaded program and any initial PC +-- and register contents, such as the ELF entry point and stack pointer the ELF +-- runners start the core with. +-- +-- Note what sharing them costs: memory and the register file are the same +-- values on both sides, and the first hop writes neither, so the invariant's +-- two container equalities hold by construction here and this property alone +-- would not notice if the core's initial register file and the ISA's +-- ('RegFile.initRF') disagreed. The concrete test in "ProofSpec" closes that +-- gap -- it runs on the real 'Vec'-backed state, where both files are built +-- independently. +baseCaseObligation :: + forall r m. (RegFileOps r, MemOps m) => r Identity -> m -> RegIdx -> Address -> Address -> Bool +baseCaseObligation rf mem wr wa pc = + driver sys == 1 && invAtFree wr wa isa sys2 + where + isa = IsaState {isaPc = pc, isaRegFile = rf, isaMem = mem} + st = (Core.init :: Core.StateG r Identity) {Core.stateFePc = pc, Core.stateRegFile = rf} + sys = Sys st Core.initInput mem + + sys1 = stepSys sys + sys2 = stepSys sys1 -- | The @k = 0@ inductive step: the driver's one-cycle hop. -- @@ -114,16 +122,16 @@ indStepObligation wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys + isa' = case isaStep isa of + Next next -> next + IsaHalted -> isa + sys' = stepSys sys premises = invAtFree wr wa isa sys && driver sys == 0 - isa' = case isaStep isa of - Next next -> next - IsaHalted -> isa - conclusion = invAtFree wr wa isa' sys' -- | The @k = 1@ inductive step: the driver's two-cycle hop. @@ -137,18 +145,18 @@ indStepObligation1 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys - s1 = stepSys sys - s2 = stepSys s1 + isa' = case isaStep isa of + Next next -> next + IsaHalted -> isa + + sys1 = stepSys sys + sys2 = stepSys sys1 premises = invAtFree wr wa isa sys && driver sys == 1 - isa' = case isaStep isa of - Next next -> next - IsaHalted -> isa - - conclusion = invAtFree wr wa isa' s2 + conclusion = invAtFree wr wa isa' sys2 -- | The @k = 2@ inductive step: the driver's three-cycle hop. -- @@ -161,19 +169,19 @@ indStepObligation2 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys - s1 = stepSys sys - s2 = stepSys s1 - s3 = stepSys s2 + isa' = case isaStep isa of + Next next -> next + IsaHalted -> isa + + sys1 = stepSys sys + sys2 = stepSys sys1 + sys3 = stepSys sys2 premises = invAtFree wr wa isa sys && driver sys == 2 - isa' = case isaStep isa of - Next next -> next - IsaHalted -> isa - - conclusion = invAtFree wr wa isa' s3 + conclusion = invAtFree wr wa isa' sys3 -- | The @k = 3@ inductive step: the driver's four-cycle hop, the longest. -- @@ -188,17 +196,17 @@ indStepObligation3 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys - s1 = stepSys sys - s2 = stepSys s1 - s3 = stepSys s2 - s4 = stepSys s3 + isa' = case isaStep isa of + Next next -> next + IsaHalted -> isa + + sys1 = stepSys sys + sys2 = stepSys sys1 + sys3 = stepSys sys2 + sys4 = stepSys sys3 premises = invAtFree wr wa isa sys && driver sys == 3 - isa' = case isaStep isa of - Next next -> next - IsaHalted -> isa - - conclusion = invAtFree wr wa isa' s4 + conclusion = invAtFree wr wa isa' sys4 diff --git a/proof/Proof/Machine.hs b/proof/Proof/Machine.hs index 66f6242..702a990 100644 --- a/proof/Proof/Machine.hs +++ b/proof/Proof/Machine.hs @@ -19,10 +19,6 @@ module Proof.Machine stepSysOut, stepSysN, initSys, - running, - exInstr, - isNopInstr, - isBubble, readMemWord, ) where @@ -30,13 +26,9 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core import Data.Functor.Identity -import Data.Maybe (isNothing) -import Data.Monoid (getFirst) -import Instruction import Memory.Types import RegFile import Types -import qualified Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) -- | Core state, the input it is about to consume, and memory. @@ -57,7 +49,6 @@ deriving instance (Show (r Identity), Show m) => Show (SysG r m) instance (Eq (r Identity), Eq m) => Eq (SysG r m) where Sys s1 i1 m1 == Sys s2 i2 m2 = s1 == s2 - && inputIsInstr i1 == inputIsInstr i2 && runIdentity (inputMem i1) == runIdentity (inputMem i2) && m1 == m2 @@ -75,18 +66,18 @@ stepSys = fst . stepSysOut stepSysOut :: (RegFileOps r, MemOps m) => SysG r m -> (SysG r m, Output Identity) stepSysOut (Sys s i m) = let (s', o) = Core.circuit s i - (i', m') = service (getFirst (outMem o)) m + (i', m') = service (outMem o) m in (Sys s' i' m', o) where - service (Just (MemAccess isInstr addr size mval)) mem = + service (Just (MemAccess _ addr size mval)) mem = case mval of -- A read. Note 'Memory.Vec.ramRead' ignores the size and always reads a -- word; the size-dependent narrowing happens in 'Core.writeback' via -- 'loadExtend'. We reproduce that here. - Nothing -> (Input isInstr (pure (memReadWord addr mem)), mem) + Nothing -> (Input (pure (memReadWord addr mem)), mem) -- A write. - Just val -> (Input isInstr (pure 0), memWriteWord size addr (runIdentity val) mem) - service Nothing mem = (Input False (pure 0), mem) + Just val -> (Input (pure 0), memWriteWord size addr (runIdentity val) mem) + service Nothing mem = (Input (pure 0), mem) stepSysN :: (RegFileOps r, MemOps m) => Int -> SysG r m -> SysG r m stepSysN n s @@ -102,27 +93,5 @@ initSys prog = sysMem = mkRAM @PROG_SIZE @RAM_SIZE_BYTES prog } -running :: SysG r m -> Bool -running = isNothing . stateHalt . sysState - -exInstr :: SysG r m -> Instruction -exInstr = stateExInstr . sysState - -isNopInstr :: Instruction -> Bool -isNopInstr (Nop _) = True -isNopInstr _ = False - --- | Is this a pipeline bubble, as opposed to a real instruction? --- --- The driver's stated invariant is \"step until the execute stage is no longer --- a no-op\", but that is slightly too coarse: @Nop DecodeFail@ is what an --- undecodable memory word decodes to, so it /is/ the architectural instruction --- at that PC and the ISA steps over it like any other. Only the stall reasons --- are genuine bubbles. -isBubble :: Instruction -> Bool -isBubble (Nop DecodeFail) = False -isBubble (Nop _) = True -isBubble _ = False - readMemWord :: Address -> MemBytes -> Word readMemWord = readWord diff --git a/proof/notes/counterexample-k0.txt b/proof/notes/counterexample-k0.txt deleted file mode 100644 index 3c37c24..0000000 --- a/proof/notes/counterexample-k0.txt +++ /dev/null @@ -1,143 +0,0 @@ -Counterexample for indStep0 (k = 0 inductive step), as reported by Z3. -===================================================================== - -SBV cannot parse array-valued variables back out of the model -("Data.SBV.interpretArray: Unable to process solver output"), so the plugin -crashes before printing a counterexample. The model is still recoverable from -the build log in two places: - - 1. The panic message embeds SBV's own s-expression parse of the array value. - 2. The [RECV] lines are Z3's raw `get-value` responses for every variable. - (Filter them back in -- we normally grep them out as noise.) - -Reproduce: uncomment the ANN on 'Verify.indStep0', then - stack build aimcore:lib > /tmp/model.txt 2>&1 - grep "^\[RECV\]" /tmp/model.txt - -DECODED MEMORY (MemArr). Everything not listed is 0. - - addr byte - 0x00000007 0x02 - 0x00000019 0x20 - 0x0000001A 0x40 - 0x7F701B31 0xB3 <-- three consecutive words, 4 bytes apart - 0x7F701B32 0x9B - 0x7F701B33 0x40 - 0x7F701B35 0x70 - 0x7F701B36 0x4F - 0x7F701B37 0xB0 - 0x7F701B39 0x80 - 0x7F701B3A 0x04 - 0x7F701B3B 0x02 - 0x7F701B3C 0x80 - 0xEFFFCFF8 0x02 - -WORDS (little-endian, as readWord assembles them): - - mem[0x7F701B31] = 0x00409BB3 opcode 0x33 -> R-type - mem[0x7F701B35] = 0x00B04F70 opcode 0x70 -> invalid -> Nop DecodeFail - mem[0x7F701B39] = 0x80020480 opcode 0x00 -> invalid -> Nop DecodeFail - -SCALARS identified so far (from [RECV]): - - s106 : Array (BitVec 5) (BitVec 32) the register file - s107 = 0x00006120 - s108 = 0x00B04F70 = mem[dePc], i.e. inputMem - s111 = 0x7F701B39 = fePc = exPc + 8 - -So the three words sit at exPc, dePc = exPc+4 and fePc = exPc+8, and the -invariant's premises (inputMem == mem[dePc], fePc == exPc+8) are satisfied. - -LEAD: the program counter is UNALIGNED -- 0x7F701B31 mod 4 == 1. The core does -not require alignment, so this is reachable in the symbolic state space even -though no realistic program produces it. Worth checking whether the invariant -needs an alignment precondition, or whether something else is at fault. - -NOT YET DONE: mapping the remaining ~141 sN variables to the property's -arguments. They are positional in declaration order, so it is mechanical but -tedious. A better route: re-run this property under the old function-schema -encoding ('Verify.mkRFPts' / 'mkMemPts'), which has no arrays -- SBV can then -decode the model itself and print a named counterexample. - - -===================================================================== -SECOND COUNTEREXAMPLE (after the load-use hazard conjunct was added) -===================================================================== - -k = 0 still comes back sat, but faster: 73s (was 131s), so the first -counterexample class is genuinely closed. - -DECODED MEMORY (all else 0): - - 0x00000001 = 0x02 - 0x04481002 = 0x04 - 0x804007C1 = 0x84 - 0xFED88070 = 0x23 <- the executing instruction starts here - 0xFED88071 = 0x30 - 0xFED88072 = 0x19 - 0xFED88073 = 0x06 - 0xFED88074 = 0x67 - -WORDS: - - mem[0xFED88070] = 0x06193023 opcode 0x23 -> S-TYPE (store), rs1=18, rs2=1 - mem[0xFED88074] = 0x00000067 opcode 0x67 -> JALR, rd=0 rs1=0 imm=0 - -So the execute stage holds a STORE this time, with the next word decoding as -jalr. Stores are the one instruction that writes memory in 'flushMeStage', and -they are also what 'Driver.storeHazard' guards, so both are worth checking: - - - does 'flushMeStage's store case agree with when 'Core.memory' actually - commits the write, the way the load case did not? - - is this another admitted-but-unreachable state, i.e. does the invariant - need a store-hazard precondition the way it now has a load-use one? - -Workflow that worked for the first one: - 1. decode the array from the panic blob (script in this repo's history) - 2. find PC anchors in the [RECV] lines - 3. rebuild concretely with MemFn/RegFn (unbounded, work concretely too) - and search the unmapped fields -- see 'ProofSpec.ceHits' - -===================================================================== -FIFTH COUNTEREXAMPLE: RESOLVED (address wraparound in noStoreAlias) -===================================================================== - -The model had exPc = 0xFFFFFFFC, dePc = 0 (wrapping), fePc = 4, a store in -the execute stage, and 0xFFFFFFFF among its unmapped 32-bit words. The -failing ingredient was the no-self-modifying-store assumption itself: - - clashes p = a < p + 4 && p < a + n -- Unsigned 32, both sums wrap - -With a PC word at the top of the address space (p = 0xFFFFFFFC), a < p + 4 -is a < 0 -- false for EVERY store address -- so a store into that word -passes the assumption unchecked. Dually, memWriteWord wraps its byte -addresses, so a word store at 0xFFFFFFFE writes bytes 0xFFFFFFFE..0x01 and -lands in a low PC word without ever satisfying p < a + n. Either way the -store rewrites an instruction word already latched into the pipeline, and -after the hop 'ex == decode (mem[isaPc])' is gone. - -Why the hand-reconstruction missed it: to satisfy the PRE-state's -'ex == decode (mem[isaPc])' (which reads the flushed memory), the store's -overlapping bytes must preserve the bytes they overwrite -- i.e. meRes must -reproduce mem's contents at the overlap -- and no such word was among the -four positional guesses tried for meRes. - -Why QuickCheck missed it: genArbSys laid out its three instruction words -with the same non-wrapping comparisons (a >= base && a < base + 4), so for -base near the top of the address space the window was empty and the premise -unsatisfiable -- the generator could not represent any state in the region -where the bug lives. - -Fixes, in proof/Invariant.hs and test/ProofSpec.hs: - - * noStoreAlias now checks each written byte with wrapping arithmetic - (byte x is in the word at p iff x - p < 4), fold-free so Pantomime can - still execute it. - * The concrete mechanism is pinned by two tests: "wrap-around aliasing - store breaks the un-guarded inductive step" (the state satisfies the - invariant, driver == 0, and the driven step breaks the invariant) and - "wrap-around aliasing store is excluded by noStoreAlias". - * genArbSys now uses a wrapping memory layout, occasionally sits the - pipeline astride 0xFFFFFFFF -> 0, biases store addresses into the PC - window, and generates branches/loads/stores in the decode slot. - 1e6 arbitrary-state tests pass after the fix. diff --git a/proof/notes/driver.txt b/proof/notes/driver.txt deleted file mode 100644 index ecbf575..0000000 --- a/proof/notes/driver.txt +++ /dev/null @@ -1,91 +0,0 @@ -DRIVER: - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateExInstr == Nop FirstCycle - THEN 1 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == True - THEN 2 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == True - THEN 2 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == True AND - isMemInstr stateExInstr == True - THEN 3 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == True AND - isMemInstr stateExInstr == False - THEN 2 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == False AND - loadHazard inputMem stateExInstr == True - THEN 3 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == False AND - loadHazard inputMem stateExInstr == False AND - isMemInstr stateWbInstr == False - THEN 0 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == False AND - loadHazard inputMem stateExInstr == False AND - isMemInstr stateWbInstr == True AND - isMemInstr stateMeInstr == False - THEN 1 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == False AND - loadHazard inputMem stateExInstr == False AND - isMemInstr stateWbInstr == True AND - isMemInstr stateMeInstr == True AND - isMemInstr stateExInstr == False - THEN 2 - -- CASE: - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isEnvInstr stateExInstr == False AND - isJumpInstr stateExInstr stateMeInstr stateMeRes stateWbInstr stateWbRes stateRegFile == False AND - storeHazard stateDePc stateExInstr stateMeInstr stateMeAddr == False AND - loadHazard inputMem stateExInstr == False AND - isMemInstr stateWbInstr == True AND - isMemInstr stateMeInstr == True AND - isMemInstr stateExInstr == True - THEN 3 \ No newline at end of file diff --git a/proof/notes/invariant.txt b/proof/notes/invariant.txt deleted file mode 100644 index dde9cc0..0000000 --- a/proof/notes/invariant.txt +++ /dev/null @@ -1,206 +0,0 @@ -NOTE: this file has been reconciled with proof/Proof/Functional/Invariant.hs. -Two changes against the original. First, the 'stateCtrl == initCtrl' clause has -been dropped from every case. It is a holdover from an earlier Core that reset the -control lines at the END of each clock cycle, so that they were back at their -reset values by the time the next cycle began. Core.withCtrlReset now resets -them at the START of the cycle and the stages then set them, so the lines seen -in any post-step state are the ones the stages left -- Core.execute alone sets -ctrlExInstr to Just every cycle. Only Core.init still satisfies the clause, so -keeping it would make the invariant hold of no state the driver lands on and -every obligation vacuous. Dropping it is sound because the lines carry no -information between cycles: withCtrlReset overwrites them before any stage -reads them. - -Second, the startup case has been removed. The invariant does not relate the -reset state to the ISA at all. Instead the base case steps the core two cycles -from reset -- the hop the driver assigns it, which fetches and decodes the first -instruction without executing anything -- and requires the running case to -relate the result to the ISA's initial state, after zero ISA steps. Every -inductive step then retires exactly one instruction. - -The four running cases are collapsed into one in the Haskell. They differ only -in the fetch conjuncts, and those track the writeback stage alone -- a memory -instruction in writeback held the bus last cycle, so nothing was fetched. The -memory stage's classification changes no conjunct; its only effect is to demand -that the stage hold something isArithOrJumpInstr or isMemInstr covers, which is -everything but ecall and ebreak. Both stages are therefore stated there as "not -an environment instruction". - -Environment instructions in the memory or writeback stage need no case of their -own: those are the intermediate cycles the driver skips, and the hop that starts -with ecall/ebreak in execute lands on the corresponding halted case below. - -See proof/Proof/Functional/Invariant.hs for the executable version, and the -"Driver and invariant" group in the test suite for the checks. - -------------------------------------------------------------------- - -isArithOrJumpInstr :: Instruction -> Bool -isArithOrJumpInstr ir = - case ir of - RType _ _ _ _ -> True - IType (Arith _) _ _ _ -> True - IType (Load _ _) _ _ _ -> False - SType _ _ _ _ -> False - BType _ _ _ _ -> True - JType _ _ -> True - IType Jump _ _ _ -> True - UType _ _ _ -> True - IType (Env Call) _ _ _ -> False - IType (Env Break _) _ _ _ -> False - Nop _ -> True - -isMemInstr :: Instruction -> Bool -isMemInstr ir = - case ir of - RType _ _ _ _ -> False - IType (Arith _) _ _ _ -> False - IType (Load _ _) _ _ _ -> True - SType _ _ _ _ -> True - BType _ _ _ _ -> False - JType _ _ -> False - IType Jump _ _ _ -> False - UType _ _ _ -> False - IType (Env Call) _ _ _ -> False - IType (Env Break _) _ _ _ -> False - Nop _ -> False - -flushWbStage :: Instruction -> Word -> Word -> (RAM, RegFile) -> (RAM, RegFile) -flushWbStage stateWbInstr stateWbRes inputMem (stateMem, stateRegFile) = - case stateWbInstr of - RType _ rd _ _ -> - (stateMem, modifyRF rd stateWbRes stateRegFile) - IType (Arith _) rd _ _ -> - (stateMem, modifyRF rd stateWbRes stateRegFile) - IType (Load size sign) rd _ _ -> - let val = loadExtend size sign inputMem - (stateMem, modifyRF rd val stateRegFile) - SType _ _ _ _ -> - (stateMem, stateRegFile) - BType _ _ _ _ -> - (stateMem, stateRegFile) - JType rd _ -> - (stateMem, modifyRF rd stateWbRes stateRegFile) - IType Jump rd _ _ -> - (stateMem, modifyRF rd stateWbRes stateRegFile) - UType _ rd _ -> - (stateMem, modifyRF rd stateWbRes stateRegFile) - IType (Env Call) _ _ _ -> - (stateMem, stateRegFile) - IType (Env Break _) _ _ _ -> - (stateMem, stateRegFile) - Nop _ -> - (stateMem, stateRegFile) - -flushMeStage :: Instruction -> Word -> Word -> (RAM, RegFile) -> (RAM, RegFile) -flushMeStage stateMeInstr stateMeRes stateMeAddr (stateMem, stateRegFile) = - case stateMeInstr of - RType _ rd _ _ -> - (stateMem, modifyRF rd stateMeRes stateRegFile) - IType (Arith _) rd _ _ -> - (stateMem, modifyRF rd stateMeRes stateRegFile) - IType (Load size sign) rd _ _ -> - let inputMem = ramRead stateMeAddr stateMem - let val = loadExtend size sign inputMem - (stateMem, modifyRF rd val stateRegFile) - SType size _ _ _ -> - (ramWrite stateMeAddr size stateMeRes stateMem, stateRegFile) - BType _ _ _ _ -> - (stateMem, stateRegFile) - JType rd _ -> - (stateMem, modifyRF rd stateMeRes stateRegFile) - IType Jump rd _ _ -> - (stateMem, modifyRF rd stateMeRes stateRegFile) - UType _ rd _ -> - (stateMem, modifyRF rd stateMeRes stateRegFile) - IType (Env Call) _ _ _ -> - (stateMem, stateRegFile) - IType (Env Break _) _ _ _ -> - (stateMem, stateRegFile) - Nop _ -> - (stateMem, stateRegFile) - -INVARIANT: - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isArithOrJumpInstr stateWbInstr == True AND - isArithOrJumpInstr stateMeInstr == True AND - stateExPc == isaPc AND - stateExInstr == decode (ramRead isaPc isaMem) AND - stateDePc == stateExPc + 4 AND - inputIsInstr == True AND - inputMem == ramRead stateDePc stateMem AND - stateFePc == stateExPc + 8 AND - loadHazard stateExInstr stateMeInstr == False AND - (isaMem, isaRegFile) == flushMemStage stateMeInstr stateMeRes stateMeAddr (flushWbStage stateWbInstr stateWbRes inputMem (stateMem, stateRegFile)) - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isMemInstr stateWbInstr == True AND - isArithOrJumpInstr stateMeInstr == True AND - stateExPc == isaPc AND - stateExInstr == decode (ramRead isaPc isaMem) AND - stateDePc == stateExPc + 4 AND - inputIsInstr == False AND - stateFePc == stateExPc + 4 AND - loadHazard stateExInstr stateMeInstr == False AND - (isaMem, isaRegFile) == flushMemStage stateMeInstr stateMeRes stateMeAddr (flushWbStage stateWbInstr stateWbRes inputMem (stateMem, stateRegFile)) - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isArithOrJumpInstr stateWbInstr == True AND - isMemInstr stateMeInstr == True AND - stateExPc == isaPc AND - stateExInstr == decode (ramRead isaPc isaMem) AND - stateDePc == stateExPc + 4 AND - inputIsInstr == True AND - inputMem == ramRead stateDePc stateMem AND - stateFePc == stateExPc + 8 AND - loadHazard stateExInstr stateMeInstr == False AND - (isaMem, isaRegFile) == flushMemStage stateMeInstr stateMeRes stateMeAddr (flushWbStage stateWbInstr stateWbRes inputMem (stateMem, stateRegFile)) - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF stateHalt == Running AND - isMemInstr stateWbInstr == True AND - isMemInstr stateMeInstr == True AND - stateExPc == isaPc AND - stateExInstr == decode (ramRead isaPc isaMem) AND - stateDePc == stateExPc + 4 AND - inputIsInstr == False AND - stateFePc == stateExPc + 4 AND - loadHazard stateExInstr stateMeInstr == False AND - (isaMem, isaRegFile) == flushMemStage stateMeInstr stateMeRes stateMeAddr (flushWbStage stateWbInstr stateWbRes inputMem (stateMem, stateRegFile)) - -------------------------------------------------------------------- -------------------------------------------------------------------- - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF isBreak (decode (ramRead isaPc isaMem)) == True AND - stateHalt == EBreak (isaPc + 4) AND - stateWbInstr == Nop Halted AND - stateMeInstr == Nop Halted AND - stateExInstr == Nop Halted AND - isaRegFile == stateRegFile AND - isaMem == stateMem - -- CASE: - (isaPc, isaRegFile, isaMem) ~ - ((stateFePc, stateDePc, stateExPc, stateExInstr, stateMeInstr, stateMeRes, stateMeAddr, stateWbInstr, stateWbRes, stateRegFile, stateCtrl, stateHalt), (inputIsInstr, inputMem), stateMem), - IF isCall (decode (ramRead isaPc isaMem)) == True AND - stateHalt == Syscall (isaPc + 4) AND - stateWbInstr == Nop Halted AND - stateMeInstr == Nop Halted AND - stateExInstr == Nop Halted AND - isaRegFile == stateRegFile AND - isaMem == stateMem diff --git a/proof/notes/leakage.txt b/proof/notes/leakage.txt deleted file mode 100644 index 4df3906..0000000 --- a/proof/notes/leakage.txt +++ /dev/null @@ -1,53 +0,0 @@ -Leakage proof: how to run it, and how to chase a failure. -========================================================= - -RUNNING -------- -Use Bitwuzla, not Z3. Z3 does not finish these queries in useful time; under -Bitwuzla each solve is seconds and symbolisation dominates. - - SBV_Z3=/opt/homebrew/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" \ - stack build aimcore:lib > /tmp/model.txt 2>&1 - grep "^\[RECV\]" /tmp/model.txt - -Build at -O1 or above. Under `stack build --fast` GHC creates no unfoldings, -the plugin cannot see through cross-module calls, and it aborts with -`Unbound variable in symbolise: ` -- a BUILD failure, easily misread as a -failed proof. - -WHAT IS PROVED --------------- -Proof.Leakage.Induction holds leakStep0..3, one per driver hop length. All four -are valid. Together with Proof.Functional.Induction.baseCase they give: -an attacker watching the memory bus learns nothing beyond Proof.Leakage.Model.L. - -The only assumption beyond the functional invariant is -Proof.Functional.Invariant.noStoreAlias -- no store writes a word the fetch path -is using -- required at every state of a hop rather than only at its ends. There -is no assumption on jump targets. - -CHASING A `sat` ---------------- -The plugin cannot print counterexamples containing arrays: SBV fails to parse -them back and the build dies with `version (...) /= storageVersion (0)`. The -model is still in the log, as the raw `get-value` responses, in SBV variable -order -- the KState fields, then Core.Input, RegArr, MemArr, then the witness -RegIdx and Address. - -Decoding that by hand is a last resort. Two cheaper moves, in order: - - 1. Split the PREMISE to find which shape fails. leakStep3a / leakStep3b in - Proof.Leakage.Induction do this on `loadHazardD`, separating the two - shapes that reach a four-cycle hop. Their annotations are commented out; - enable them to reproduce. - - 2. Split the CONCLUSION to find which conjunct fails -- the state equality or - one of the four observation slots. Assume the full premises and assert one - piece at a time. - -Then reproduce concretely with test/LeakageSpec.hs, whose arbitrary-state -generators range over the same space the symbolic properties quantify over -(unreachable states included) and give a shrunk, printable counterexample. If -the search cannot find it, the generator is missing a shape: check that the -instruction forms involved are actually generated before concluding the state -is unreachable. From f3dc4886a5ef4b3567416afc9f07897df16ed984 Mon Sep 17 00:00:00 2001 From: Kristina Date: Fri, 9 Oct 2026 23:43:46 +0200 Subject: [PATCH 3/8] Rewrite the leakage proof at ISA level Replace the old leakage proof, which ran the core on a censored state, with a simulation against a separate, leakage-only simulator: - Proof.Leakage.Model: the per-cycle bus observation Obs (with its first-access-wins Semigroup) and the ISA-level Leak of an instruction, computed by leakOf from the architectural state. - Proof.Leakage.Simulator: a pipeline with the core's stage structure and timing that sees only the leakage of the instruction entering its execute stage, and emits one Obs per cycle. - Proof.Leakage.Driver: simDriver, the simulator's counterpart of the functional driver, case for case. - Proof.Leakage.Invariant: simInv, relating the simulator to the core (PCs, whether decode expects an instruction, running or halted, and the pending memory access). - Proof.Leakage.Obligation: a base case for the first hop from the initial state, and one step per hop length. Each step assumes the functional invariant, the driver's delay and simInv, and shows that simDriver agrees, every cycle's observation matches, and simInv holds again. - proof-smt/Proof/Leakage/Induction.hs: the symbolic properties, replacing the disabled module. Bitwuzla discharges the base case and all four steps. Co-Authored-By: Claude Opus 5.5 --- proof-smt/Proof/Leakage/Induction.hs | 97 ++++ proof/Proof/Leakage/Driver.hs | 51 ++ proof/Proof/Leakage/Induction.hs-disabled | 162 ------ proof/Proof/Leakage/Invariant.hs | 52 ++ proof/Proof/Leakage/Model.hs | 324 ++++------- proof/Proof/Leakage/Obligation.hs | 204 +++++-- proof/Proof/Leakage/Simulator.hs | 636 ++++++++++------------ 7 files changed, 757 insertions(+), 769 deletions(-) create mode 100644 proof-smt/Proof/Leakage/Induction.hs create mode 100644 proof/Proof/Leakage/Driver.hs delete mode 100644 proof/Proof/Leakage/Induction.hs-disabled create mode 100644 proof/Proof/Leakage/Invariant.hs diff --git a/proof-smt/Proof/Leakage/Induction.hs b/proof-smt/Proof/Leakage/Induction.hs new file mode 100644 index 0000000..dae284c --- /dev/null +++ b/proof-smt/Proof/Leakage/Induction.hs @@ -0,0 +1,97 @@ +-- | The leakage proof, checked symbolically. +-- +-- 'baseCaseLeak' plus one property per driver delay: on a hop of that length, +-- the corresponding obligation in "Proof.Leakage.Obligation" holds. Split by +-- @k@ because the number of unrolled cycles has to be concrete -- Pantomime +-- cannot recurse on a symbolic count -- and each property pins @driver == k@ so +-- it carries one unrolling rather than four. +-- +-- Together with "Proof.Functional.Induction" these are the leakage theorem: the +-- functional proof establishes that the invariant holds wherever the driver +-- lands, which each step here assumes as a premise. +-- +-- Each query runs both the core and the simulator over the hop and compares +-- their per-cycle bus observations, the two drivers' hop lengths and the +-- simulator invariant, so they are larger than the corresponding functional +-- ones. The statements live in "Proof.Leakage.Obligation"; this module only +-- instantiates them. +-- +-- The system state is passed as a 'KState' plus SMT-array register file and +-- memory (see "Proof.SMT.System"); the simulator state is passed directly, +-- since it holds no register file or memory. +-- +-- == Running them +-- +-- Under Bitwuzla, not Z3: +-- +-- > SBV_Z3=/usr/local/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" stack build +module Proof.Leakage.Induction + ( baseCaseLeak, + indStepLeak, + indStepLeak1, + indStepLeak2, + indStepLeak3, + results, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import qualified Core +import Data.Functor.Identity +import Pantomime (Theory (..)) +import qualified Pantomime.BuiltIn as Pantomime +import Proof.Leakage.Obligation +import Proof.Leakage.Simulator +import Proof.SMT.Array +import Proof.SMT.Axioms (arrayAxioms) +import Proof.SMT.Logged (pantomime) +import Proof.SMT.System +import Types +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- The base case ---------------------------------------------------------------- + +-- | The first hop from the initial state, for any start PC, register file and +-- memory. +{-# ANN baseCaseLeak (Theory arrayAxioms) #-} +baseCaseLeak :: RegArr -> MemArr -> Address -> Pantomime.Bool +baseCaseLeak ra ma pc = + Pantomime.boolean $ baseCaseLeakObligation (RegArrF ra) ma pc + +-- The inductive steps ---------------------------------------------------------- + +-- | @k = 0@: the one-cycle hop (steady, writeback non-memory). +{-# ANN indStepLeak (Theory arrayAxioms) #-} +indStepLeak :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool +indStepLeak ss i ra ma wr wa ipc sim = + Pantomime.boolean $ indStepLeakObligation wr wa ipc (sysOf ss i ra ma) sim + +-- | @k = 1@: the two-cycle hop (a memory instruction in writeback). +{-# ANN indStepLeak1 (Theory arrayAxioms) #-} +indStepLeak1 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool +indStepLeak1 ss i ra ma wr wa ipc sim = + Pantomime.boolean $ indStepLeakObligation1 wr wa ipc (sysOf ss i ra ma) sim + +-- | @k = 2@: the three-cycle hop (environment, taken jump, store hazard with a +-- non-memory execute instruction, or memory instructions in both older stages). +-- The hop on which the ISA enters a halt; a halted state then sits at k = 0. +{-# ANN indStepLeak2 (Theory arrayAxioms) #-} +indStepLeak2 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool +indStepLeak2 ss i ra ma wr wa ipc sim = + Pantomime.boolean $ indStepLeakObligation2 wr wa ipc (sysOf ss i ra ma) sim + +-- | @k = 3@: the four-cycle hop (store hazard with a memory execute +-- instruction, load hazard, or all three stages holding memory instructions). +{-# ANN indStepLeak3 (Theory arrayAxioms) #-} +indStepLeak3 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool +indStepLeak3 ss i ra ma wr wa ipc sim = + Pantomime.boolean $ indStepLeakObligation3 wr wa ipc (sysOf ss i ra ma) sim + +results :: [(String, Maybe String)] +results = + [ ("baseCaseLeak", $(pantomime 'baseCaseLeak)), + ("indStepLeak", $(pantomime 'indStepLeak)), + ("indStepLeak1", $(pantomime 'indStepLeak1)), + ("indStepLeak2", $(pantomime 'indStepLeak2)), + ("indStepLeak3", $(pantomime 'indStepLeak3)) + ] diff --git a/proof/Proof/Leakage/Driver.hs b/proof/Proof/Leakage/Driver.hs new file mode 100644 index 0000000..b23e0a4 --- /dev/null +++ b/proof/Proof/Leakage/Driver.hs @@ -0,0 +1,51 @@ +-- | The simulator's driver: how many cycles the simulator takes for an +-- instruction, computed from its own state and the instruction's leakage. The +-- counterpart of 'Proof.Functional.Driver.driver', case for case; the leakage +-- proof's first step is that the two agree. +module Proof.Leakage.Driver + ( simDriver, + simStoreHazard, + simLoadHazard + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import qualified Instruction +import Proof.Leakage.Model +import Proof.Leakage.Simulator +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | The store-hazard condition of 'Core.decode': the instruction word at the +-- decode-stage PC overlaps a store either in the execute stage or in the memory +-- stage. +simStoreHazard :: SimInput -> SimState -> Bool +simStoreHazard inp st = + maybe False (Instruction.storeHazard dePc) exStore + || maybe False (Instruction.storeHazard dePc) meStore + where + dePc = simStateDePc st + exStore = case inp of + Just (LStore size addr) -> Just (addr, size) + _ -> Nothing + meStore = case simStateMeInstr st of + LStore size addr -> Just (addr, size) + _ -> Nothing + +-- | The load-hazard condition of 'Core.decode', computed by the ISA as part of +-- the leakage. +simLoadHazard :: SimInput -> SimState -> Bool +simLoadHazard (Just (LLoad _ _ haz)) st = simStateDeExpInstr st && haz +simLoadHazard _ _ = False + +simDriver :: SimInput -> SimState -> Int +simDriver inp st + | simStateExInstrType st == FirstCycle = 1 + | simStateExInstrType st == Halted = 0 + | maybe False isEnvLeak inp = 2 + | maybe False isJumpLeak inp = 2 + | simStoreHazard inp st = if maybe False isMemLeak inp then 3 else 2 + | simLoadHazard inp st = 3 + | simStateDeExpInstr st = 0 + | not (isMemLeak (simStateMeInstr st)) = 1 + | not (maybe False isMemLeak inp) = 2 + | otherwise = 3 diff --git a/proof/Proof/Leakage/Induction.hs-disabled b/proof/Proof/Leakage/Induction.hs-disabled deleted file mode 100644 index 3d427b9..0000000 --- a/proof/Proof/Leakage/Induction.hs-disabled +++ /dev/null @@ -1,162 +0,0 @@ --- | The leakage refinement, checked symbolically. --- --- One property per driver delay: on a hop of that length, --- 'Proof.Leakage.Obligation.leakObligation' holds. Split by @k@ because the --- number of unrolled cycles has to be concrete -- Pantomime cannot recurse on a --- symbolic count -- and each property pins @driver == k@ so it carries one --- unrolling rather than four. --- --- These four plus 'Proof.Functional.Induction.baseCase' are the leakage --- theorem: the functional half establishes that the invariant holds wherever --- the driver lands, which is what each property here assumes. --- --- == Running them --- --- Under Bitwuzla, not Z3: --- --- > SBV_Z3=/opt/homebrew/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" stack build --- --- Z3 does not finish these in useful time; under Bitwuzla each solve is seconds --- and symbolisation dominates. The whole module is well under an hour. --- --- Each query runs the pipeline twice over -- once on the real state, once on --- the censored one -- and compares two states plus two observation traces, so --- they are larger than the corresponding 'Proof.Functional.Induction' ones. --- They are stated in the form the QuickCheck harness (@test/LeakageSpec.hs@) --- checks, so a counterexample to one is a counterexample to the other; when a --- query comes back @sat@, splitting the premise or the conclusion localises it --- faster than decoding the model (see @proof/notes/leakage.txt@). -module Proof.Leakage.Induction - ( leakStep0, - leakStep1, - leakStep2, - leakStep3, - leakStep3a, - leakStep3b, - results, - ) -where - -import Proof.SMT.Array -import Proof.SMT.Axioms (arrayAxioms) -import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) -import qualified Core -import Data.Functor.Identity -import Proof.Driver (driver, loadHazardD) -import Instruction -import Proof.Leakage.Obligation (leakObligation) -import Proof.SMT.Logged (pantomime) -import Proof.Machine -import Pantomime (Theory (..)) -import qualified Pantomime.BuiltIn as Pantomime -import RegFile (RegFileOps) -import Types -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) - --- | The pipeline registers, as plain scalars. --- --- An ADT of scalars can be a fresh symbolic argument; a record containing a --- function cannot, and the Clash @Vec@ API is opaque to the plugin. Same shape --- and same reason as 'Proof.Functional.Induction'\'s. -data KState = KState - { kFePc :: Address, - kDePc :: Address, - kExPc :: Address, - kExIr :: Instruction, - kMeIr :: Instruction, - kMeRes :: Word, - kMeAddr :: Address, - kWbIr :: Instruction, - kWbRes :: Word, - kCtrl :: Core.Control Identity, - kHalt :: Maybe Core.HaltState, - kHaltNextPc :: Address - } - -sysOf :: KState -> Core.Input Identity -> RegArr -> MemArr -> SysG RegArrF MemArr -sysOf ss i ra ma = - Sys - { sysState = - Core.State - { Core.stateFePc = kFePc ss, - Core.stateDePc = kDePc ss, - Core.stateExPc = kExPc ss, - Core.stateExInstr = kExIr ss, - Core.stateMeInstr = kMeIr ss, - Core.stateMeRes = Identity (kMeRes ss), - Core.stateMeAddr = kMeAddr ss, - Core.stateWbInstr = kWbIr ss, - Core.stateWbRes = Identity (kWbRes ss), - Core.stateRegFile = RegArrF ra, - Core.stateCtrl = kCtrl ss, - Core.stateHalt = kHalt ss, - Core.stateHaltNextPc = kHaltNextPc ss - }, - sysInput = i, - sysMem = ma - } - --- | 'Proof.Leakage.Obligation.leakObligation', restricted to hops of length --- @k + 1@. -leakAt :: - (RegFileOps r, MemOps m) => - Int -> RegIdx -> Address -> SysG r m -> Bool -leakAt k wr wa sys = driver sys /= k || leakObligation wr wa sys - --- | @k = 0@: the one-cycle hop. -{-# ANN leakStep0 (Theory arrayAxioms) #-} -leakStep0 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep0 ss i ra ma wr wa = - Pantomime.boolean $ leakAt 0 wr wa (sysOf ss i ra ma) - --- | @k = 1@: the two-cycle hop (startup, or a memory instruction in writeback). -{-# ANN leakStep1 (Theory arrayAxioms) #-} -leakStep1 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep1 ss i ra ma wr wa = - Pantomime.boolean $ leakAt 1 wr wa (sysOf ss i ra ma) - --- | @k = 2@: the three-cycle hop -- an environment instruction, a taken jump, --- or a store hazard. The store-hazard route was unreachable while the aliasing --- assumption stood; it is live now. -{-# ANN leakStep2 (Theory arrayAxioms) #-} -leakStep2 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep2 ss i ra ma wr wa = - Pantomime.boolean $ leakAt 2 wr wa (sysOf ss i ra ma) - --- | @k = 3@: the four-cycle hop -- a load-use hazard, or memory instructions in --- all three older stages. -{-# ANN leakStep3 (Theory arrayAxioms) #-} -leakStep3 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep3 ss i ra ma wr wa = - Pantomime.boolean $ leakAt 3 wr wa (sysOf ss i ra ma) - --- | @k = 3@ restricted to the load-use-hazard route. --- --- Kept, with its annotation off, as a worked example of localising a @sat@ --- result: splitting @leakStep3@ on 'Proof.Driver.loadHazardD' says which of the --- two shapes that reach a four-cycle hop is at fault, which is quicker than --- decoding an array-valued model. --- {-# ANN leakStep3a (Theory arrayAxioms) #-} -leakStep3a :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep3a ss i ra ma wr wa = - Pantomime.boolean $ - let sys = sysOf ss i ra ma - in not (loadHazardD sys) || leakAt 3 wr wa sys - --- | @k = 3@ restricted to the steady all-memory route. --- {-# ANN leakStep3b (Theory arrayAxioms) #-} -leakStep3b :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool -leakStep3b ss i ra ma wr wa = - Pantomime.boolean $ - let sys = sysOf ss i ra ma - in loadHazardD sys || leakAt 3 wr wa sys - --- | Verdicts, spliced in by the plugin at compile time: 'Nothing' when the --- property is valid, @'Just' counterexample@ when it is not. -results :: [(String, Maybe String)] -results = - [ ("leakStep0", $(pantomime 'leakStep0)), - ("leakStep1", $(pantomime 'leakStep1)), - ("leakStep2", $(pantomime 'leakStep2)), - ("leakStep3", $(pantomime 'leakStep3)) - ] diff --git a/proof/Proof/Leakage/Invariant.hs b/proof/Proof/Leakage/Invariant.hs new file mode 100644 index 0000000..5ba9c61 --- /dev/null +++ b/proof/Proof/Leakage/Invariant.hs @@ -0,0 +1,52 @@ +-- | The invariant relating the leakage simulator to the core: the leakage +-- counterpart of "Proof.Functional.Invariant". +module Proof.Leakage.Invariant + ( simInv + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core +import Data.Maybe (isJust, isNothing) +import Instruction hiding (Halted) +import Proof.Leakage.Model +import Proof.Leakage.Simulator +import Proof.Machine +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | The relation between the simulator and the core that the leakage proof +-- preserves from hop to hop. +-- +-- The two machines fetch and decode at the same PCs, agree on whether decode +-- expects an instruction, are both running or both halted, and have the same +-- memory access pending in the memory stage. Which instruction the core is +-- executing is not stated here: the functional invariant pins the core's +-- execute stage to the ISA's next instruction, and the simulator is fed that +-- instruction's leakage, so the two agree by construction. +-- +-- The simulator has no writeback stage; 'simStateDeExpInstr' stands in for the +-- one fact about it the driver needs. Stall states are excluded: the relation +-- is only stated at hop boundaries, where the execute stage holds a decoded +-- instruction or the core has halted. +simInv :: + SimState -> + SysG r m -> + Bool +simInv sim (Sys st _ _) = + simStateFePc sim == stateFePc st + && simStateDePc sim == stateDePc st + && simStateDeExpInstr sim == stateDeExpInstr st + && exStage + && meStage + where + exStage = case simStateExInstrType sim of + DecodedInstr -> isNothing (stateHalt st) + Halted -> isJust (stateHalt st) + _ -> False + + meStage = case (simStateMeInstr sim, stateMeInstr st) of + (LLoad size addr _, Instruction.IType (Load size' _) _ _ _) -> + size == size' && addr == stateMeAddr st + (LStore size addr, Instruction.SType size' _ _ _) -> + size == size' && addr == stateMeAddr st + (leak, ir) -> not (isMemLeak leak) && not (Instruction.isMemInstr ir) diff --git a/proof/Proof/Leakage/Model.hs b/proof/Proof/Leakage/Model.hs index 0531af0..4d77cb4 100644 --- a/proof/Proof/Leakage/Model.hs +++ b/proof/Proof/Leakage/Model.hs @@ -1,258 +1,156 @@ --- | What the core leaks, what an attacker sees, and how to invert one into the --- other. +-- | What an attacker sees, and what one architectural instruction leaks. -- -- The leakage proof ("Proof.Leakage.Obligation") establishes that an attacker --- watching the memory bus learns nothing beyond 'L'. This module defines the --- three functions that statement is about: --- --- * 'obsOf' -- what the attacker sees in one cycle. --- * 'leakOf' -- what one architectural instruction leaks. A function of the --- ISA state alone; the pipeline does not appear in it. --- * 'inv' -- a representative instruction with the same leakage as the real --- one. The simulator runs the unmodified core on these, so anything 'inv' --- cannot express is something the proof cannot cover. +-- watching the memory bus learns nothing beyond 'Leak'. Two definitions carry +-- that statement: +-- +-- * 'obsOf' -- what the attacker sees in one cycle: the kind of access, its +-- address, and for a data access its width. +-- * 'leakOf' -- what the instruction an architectural state is about to +-- process leaks. A function of the ISA state alone; the pipeline does not +-- appear in it. +-- +-- 'Leak' follows the observation rather than the instruction set. Control flow +-- shows up only as the next fetch address, so a taken branch and a jump are the +-- same thing ('LJump' with the target) and an untaken branch is +-- indistinguishable from arithmetic ('LArith'). A load or store shows its data +-- address; a load also carries whether the instruction at @pc + 4@ has a +-- load-use hazard against it, which is the one thing the fetch trace does not +-- already give away, since it decides how long the hop takes. +-- +-- == What 'Leak' is, and is not +-- +-- It is not a list of secrets. Every field is public in any run that does not +-- halt, because 'Core.execute' computes each one inside @noSecrets'@: the +-- branch condition, the @jalr@ target, and the load and store addresses. The +-- fetched instruction word goes through @noSecrets'@ in 'Core.decode' too, so +-- the program is public even under self-modifying code -- which matters, because +-- store /data/ is not forced public, so a store could otherwise plant a +-- secret-dependent instruction. A secret reaching any of these halts the core +-- with 'Core.SecurityViolation'. The hazard bit is not even data dependent: +-- 'Instruction.loadHazard' compares register /fields/, not their contents. +-- +-- So 'Leak' is what the /simulator/ needs in order to replay the observation +-- from the architectural state alone, not what escapes. The security content +-- lives in the @Access@ / @noSecrets@ discipline. module Proof.Leakage.Model ( -- * Observation Obs (..), - HopObs (..), obsOf, -- * Leakage - Class (..), - L (..), + Leak (..), leakOf, - mkDeps, - isaClass, - coreClass, - - -- * Inversion - inv, - invWord, - jumpSource, + isJumpLeak, + isMemLeak, + isEnvLeak ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core import Data.Functor.Identity -import Data.Maybe (fromMaybe) -import Data.Monoid (getFirst) import Instruction -import qualified Instruction as I -import Proof.Driver (exArg) import ISA (IsaStateG (..), isaInstrAt) import Memory.Types (MemOps (..)) -import Proof.Machine import RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) -- Observation ----------------------------------------------------------------- --- | What the attacker sees on the memory bus in one cycle. --- --- An instruction fetch shows its address -- this is the program-counter trace. --- A data access shows only its kind and width: neither the address nor the --- value. --- --- Data addresses are excluded because the simulator could not reproduce them. --- A load or store computes its address as @register + immediate@, and 'inv' --- emits instructions that read a censored register file; a jump target escapes --- that limit only because 'jumpSource' parks it in a register first, which --- works for at most one instruction per hop. +-- | What the attacker sees on the memory bus in one cycle: the kind of access, +-- its address, and for a data access its width. data Obs = NoAccess | Fetch Address - | DataRead Size - | DataWrite Size + | DataRead Address Size + | DataWrite Address Size deriving (Eq, Show, Generic, NFDataX) --- | The observations of one driver hop, one slot per cycle. --- --- A hop is one to four cycles. Four slots rather than a list because Pantomime --- cannot execute folds; 'Nothing' means the hop was not that long, so hops of --- different lengths compare unequal. -data HopObs = HopObs (Maybe Obs) (Maybe Obs) (Maybe Obs) (Maybe Obs) - deriving (Eq, Show, Generic, NFDataX) +instance Semigroup Obs where + NoAccess <> obs' = obs' + obs <> _ = obs + +instance Monoid Obs where + mempty = NoAccess -- | The observation a cycle's 'Core.Output' produces. obsOf :: Output Identity -> Obs -obsOf o = case getFirst (outMem o) of +obsOf o = case outMem o of Nothing -> NoAccess Just (MemAccess True addr _ _) -> Fetch addr - Just (MemAccess False _ size Nothing) -> DataRead size - Just (MemAccess False _ size (Just _)) -> DataWrite size + Just (MemAccess False addr size Nothing) -> DataRead addr size + Just (MemAccess False addr size (Just _)) -> DataWrite addr size -- Leakage --------------------------------------------------------------------- --- | The class of one architectural instruction: what the attacker learns about --- it beyond its own existence. --- --- Each constructor carries what the simulator needs and no more: --- --- * 'CBranchTaken' and 'CJal' carry the instruction's own immediate, a field --- of the instruction word rather than a function of register contents. --- 'CBranchNotTaken' carries nothing, since an untaken branch's target is --- not observable. --- * 'CJalr' carries a computed address. This one is genuinely data --- dependent -- it is the leak. --- * 'CLoad' carries its destination register, because a load-use hazard --- against the next instruction depends on it and that decides how many --- cycles the next hop takes. It carries no address. --- * Sizes are carried because 'Obs' shows the access width. -data Class - = CPlain - | CBranchTaken BImm - | CBranchNotTaken - | CJal JImm - | CJalr Address - | CLoad Size RegIdx - | CStore Size - | CCall - | CBreak +-- | What one architectural instruction leaks. +-- +-- The constructors are named for what reaches the observation, not for the +-- instruction set: +-- +-- * 'LArith' -- nothing beyond the fetch trace. No data access, and the next +-- fetch is @pc + 4@. Arithmetic, upper immediates, an untaken branch, and an +-- undecodable word all land here, and are indistinguishable. +-- * 'LJump' -- control goes somewhere other than @pc + 4@, and the target is +-- the next fetch address. A taken branch, @jal@ and @jalr@ are one case: the +-- attacker sees an address, not which instruction produced it. +-- * 'LLoad' -- a data read of the given width at the given address, plus +-- whether the instruction at @pc + 4@ has a load-use hazard against this +-- load. That bit is the one thing here not already in the fetch trace: it +-- decides how many cycles the hop takes, and the timing is observable. +-- * 'LStore' -- a data write of the given width at the given address. The +-- value written is not observable and is not carried. +-- * 'LEnv' -- @ecall@ or @ebreak@. The core halts, so no fetch follows. +data Leak + = LArith + | LJump Address + | LLoad Size Address Bool + | LStore Size Address + | LEnv deriving (Eq, Show, Generic, NFDataX) --- | An instruction's class together with the source registers it may depend on. --- --- The dependencies are leaked for every instruction, not only those that use --- them: 'Core.decode' compares them against the destination register of a load --- in the execute stage, and that comparison decides the hop length. -data L = L - { lClass :: Class, - lDeps :: (Maybe RegIdx, Maybe RegIdx) - } - deriving (Eq, Show, Generic, NFDataX) +isJumpLeak :: Leak -> Bool +isJumpLeak (LJump _) = True +isJumpLeak _ = False --- | An instruction's source registers, with @x0@ dropped -- reading @x0@ can --- never be a hazard. Matches the filter in 'Instruction.loadHazard', which is --- the consumer that matters. --- --- Note this reads the registers through 'Instruction.getRs1' and --- 'Instruction.getRs2', which do not always answer with the encoded fields: --- @ecall@ reports @x17@ whatever is encoded, and a @Nop@ reports @x0@. -mkDeps :: Instruction -> (Maybe RegIdx, Maybe RegIdx) -mkDeps ir = (noZero (getRs1 ir), noZero (getRs2 ir)) - where - noZero (Just 0) = Nothing - noZero r = r +isMemLeak :: Leak -> Bool +isMemLeak (LLoad {}) = True +isMemLeak (LStore {}) = True +isMemLeak _ = False + +isEnvLeak :: Leak -> Bool +isEnvLeak LEnv = True +isEnvLeak _ = False -- | The leakage of the instruction an architectural state is about to process. -leakOf :: (RegFileOps r, MemOps m) => IsaStateG r m -> L -leakOf isa = L (isaClass isa ir) (mkDeps ir) +leakOf :: (RegFileOps r, MemOps m) => IsaStateG r m -> Leak +leakOf isa@(IsaState pc rf _) = + case ir of + RType {} -> LArith + IType (Arith _) _ _ _ -> LArith + UType {} -> LArith + BType cmp imm rs1 rs2 -> + let doBranch = runIdentity $ branch cmp (pure (regv rs1)) (pure (regv rs2)) + in if doBranch + then LJump (pc + off imm) + else LArith + JType _ imm -> + LJump (pc + off imm) + IType Jump _ rs1 imm -> + LJump (addr rs1 imm) + IType (Load size _) _ rs1 imm -> + let hazard = loadHazard (isaInstrAt isa {isaPc = pc + 4}) ir + in LLoad size (addr rs1 imm) hazard + SType size imm rs1 _ -> + LStore size (addr rs1 imm) + IType (Env _) _ _ _ -> LEnv + -- An undecodable word decodes to @Nop DecodeFail@, which is a real + -- architectural instruction and leaks like any other non-memory one. + Nop _ -> LArith where ir = isaInstrAt isa - --- | Classify an instruction against the architectural state it runs in. --- --- Three decisions are data dependent -- whether a branch is taken, and the two --- computed jump targets -- and are resolved here against the architectural --- register file. 'coreClass' resolves the same three against forwarded pipeline --- values, and the proof shows they agree. -isaClass :: (RegFileOps r, MemOps m) => IsaStateG r m -> Instruction -> Class -isaClass (IsaState _ rf _) ir = case ir of - BType cmp imm rs1 rs2 -> - if runIdentity (branch cmp (pure (regv rs1)) (pure (regv rs2))) - then CBranchTaken imm - else CBranchNotTaken - JType _ imm -> CJal imm - IType Jump _ rs1 imm -> CJalr (unpack (regv rs1 + signExtend imm)) - IType (Load size _) rd _ _ -> CLoad size rd - SType size _ _ _ -> CStore size - IType (Env Call) _ _ _ -> CCall - IType (Env Break) _ _ _ -> CBreak - _ -> CPlain - where regv i = runIdentity (lookupRFg i rf) - --- | Classify the execute-stage instruction against a core state. --- --- The mirror of 'isaClass'. Operands are read through 'Proof.Driver.exArg', --- which reproduces the forwarding priority 'Core.execute' uses. -coreClass :: (RegFileOps r) => SysG r m -> Instruction -> Class -coreClass sys ir = case ir of - BType cmp imm rs1 rs2 -> - if runIdentity (branch cmp (pure (exArg sys rs1)) (pure (exArg sys rs2))) - then CBranchTaken imm - else CBranchNotTaken - JType _ imm -> CJal imm - IType Jump _ rs1 imm -> CJalr (unpack (exArg sys rs1 + signExtend imm)) - IType (Load size _) rd _ _ -> CLoad size rd - SType size _ _ _ -> CStore size - IType (Env Call) _ _ _ -> CCall - IType (Env Break) _ _ _ -> CBreak - _ -> CPlain - --- Inversion ------------------------------------------------------------------- - --- | A representative instruction with the same leakage as the real one. --- --- The simulator's register file holds zero everywhere except the one slot --- 'jumpSource' reserves, so every instruction here is chosen to behave --- independently of register contents: --- --- * @'CBranchTaken' imm@ becomes @beq d1, d2, imm@. Both operands read zero, --- so it is always taken, and the original immediate takes it to the --- original target. @'CBranchNotTaken'@ becomes @bne d1, d2, 0@, never taken --- for the same reason. --- * @'CJal'@ keeps its immediate, which is PC-relative and needs no register. --- * @'CJalr'@ addresses @0(src)@ and reads its target out of @src@; see --- 'jumpSource'. When the real @jalr@ read @x0@ there is no register to use, --- but then the target is @0 + signExtend imm@ and fits the immediate --- exactly. --- * @'CLoad'@ and @'CStore'@ address @0(rs1)@, i.e. address zero. The address --- is not observable; the width and the fact that it is a memory instruction --- are, and both survive. --- --- Destination registers are @x0@ except for a load, whose destination is --- leaked because it drives the next hop's hazard. A load into a real register --- writes @loadExtend size sign 0 == 0@, so the register file stays zero. --- --- Source registers are threaded through everywhere so that a load-use hazard --- against this instruction fires in the simulator exactly when it fires in the --- core. -inv :: L -> Instruction -inv (L cls (d1, d2)) = case cls of - CPlain -> RType ADD 0 (r d1) (r d2) - CBranchTaken imm -> BType EQ imm (r d1) (r d2) - CBranchNotTaken -> BType NE 0 (r d1) (r d2) - CJal imm -> JType 0 imm - CJalr t -> case d1 of - Just src | src /= 0 -> IType Jump 0 src 0 - _ -> IType Jump 0 0 (slice d11 d0 (pack t)) - CLoad size rd -> IType (Load size I.Signed) rd (r d1) 0 - CStore size -> SType size 0 (r d1) (r d2) - CCall -> IType (Env Call) 0 0 0 - -- The immediate is the opcode rather than a value: 'Instruction.decode' reads - -- @ecall@ off @immI == 0@ and @ebreak@ off @immI == 1@ and re-emits it, so a - -- zero here would not survive 'invWord'. - -- - -- Unlike @ecall@, an @ebreak@ reports its encoded @rs1@ from - -- 'Instruction.getRs1', so that field is a real dependency and has to be - -- threaded through like any other. - CBreak -> IType (Env Break) 0 (r d1) 1 - where - r = fromMaybe 0 - --- | The word the simulator puts on the bus for 'Core.decode' to read. --- --- @'Instruction.decode'' . 'invWord'@ is 'inv': every instruction 'inv' emits --- survives the round trip. -invWord :: L -> Word -invWord l = case encode' (inv l) of - Just w -> w - Nothing -> 0 - --- | The register a leaked @jalr@ target has to be parked in, and the target. --- --- No RISC-V instruction word can hold a 32-bit jump target: every target the --- core computes is @PC + immediate@ (13 bits for a branch, 21 for @jal@) or --- @register + immediate@ (12 bits for @jalr@). The register file is therefore --- the only place an arbitrary target fits, and @jalr@ is the one instruction --- that reads it from there. Writing it costs nothing in leakage: the value is --- the target, which 'L' already carries. --- --- 'Nothing' for everything else, including a @jalr@ off @x0@, where the target --- fits the immediate and nothing needs parking. -jumpSource :: L -> Maybe (RegIdx, Address) -jumpSource (L (CJalr t) (Just src, _)) | src /= 0 = Just (src, t) -jumpSource _ = Nothing + off imm = unpack $ signExtend imm + addr rs1 imm = unpack $ regv rs1 + signExtend imm diff --git a/proof/Proof/Leakage/Obligation.hs b/proof/Proof/Leakage/Obligation.hs index df6ea0f..e50b451 100644 --- a/proof/Proof/Leakage/Obligation.hs +++ b/proof/Proof/Leakage/Obligation.hs @@ -1,58 +1,180 @@ --- | The leakage theorem, as a preservation obligation. +-- | The leakage proof obligations, in one place. -- --- 'leakObligation' says that 'Proof.Leakage.Simulator.proj' commutes with one --- driver hop: if it relates an implementation state to an architectural state --- and a simulator state, then after the hop it relates them again, and the two --- machines produced the same cycle-by-cycle observations. +-- The leakage theorem: an attacker watching the memory bus learns nothing +-- beyond the ISA-level leakage. Stated as a simulation: the simulator, which +-- sees only 'leakOf' of the ISA state, produces the same bus observation as the +-- core on every cycle, and takes the same number of cycles per instruction. -- --- Together with the invariant holding at reset, that gives the leakage result: --- an attacker watching the memory bus learns nothing that is not already in --- 'Proof.Leakage.Model.L'. The simulator reproduces the observation from the --- leakage alone, including the hop length -- which is the instruction timing. --- --- Only the simulator half of the projection is checked here. The architectural --- half commutes by construction: 'Proof.Leakage.Simulator.archOfLeak' is --- 'Proof.Functional.Obligation.isaAt' at 'Proof.Functional.Obligation.hopPc', composed with --- 'Proof.Leakage.Simulator.isaNext', and the functional obligations already --- establish that it advances by one 'isaStep' per hop. --- --- == What is assumed --- --- Nothing beyond the invariant. A store overlapping the instruction word in --- decode is caught by 'Core.decode' and stalled, so the aliasing-store side --- condition the earlier proof carried is gone. --- --- There is deliberately no assumption on jump targets. Branch and @jal@ targets --- are reproduced with the original immediates; a @jalr@ target is parked in a --- register by 'Proof.Leakage.Simulator.installJump' and is exact for any 32-bit --- address. +-- Each inductive step assumes the functional invariant ('invAtFree') as a +-- premise. It pins the core's execute stage to the ISA's next instruction, so +-- feeding the simulator that instruction's leakage keeps the two machines in +-- step. The functional proof supplies the invariant for the next hop, so it is +-- not re-proved here. 'simInv' carries the rest from hop to hop. module Proof.Leakage.Obligation - ( leakObligation, - leakPremises, + ( baseCaseLeakObligation, + indStepLeakObligation, + indStepLeakObligation1, + indStepLeakObligation2, + indStepLeakObligation3 ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core +import Data.Functor.Identity +import Memory.Types (MemOps (..)) +import Proof.Functional.Driver import Proof.Functional.Invariant (invAtFree) -import Proof.Functional.Obligation (hopPc, isaAt) +import Proof.Functional.Obligation +import Proof.Leakage.Driver +import Proof.Leakage.Invariant import Proof.Leakage.Model import Proof.Leakage.Simulator -import Memory.Types (MemOps (..)) import Proof.Machine import RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) --- | The premises of 'leakObligation': the functional invariant. -leakPremises :: - (RegFileOps r, MemOps m) => RegIdx -> Address -> SysG r m -> Bool -leakPremises wr wa sys = invAtFree wr wa (isaAt (hopPc sys) sys) sys +-- | The base case: from the initial state, the core and the simulator agree +-- on the first hop. +-- +-- Both start from their initial states with the same start PC. Over the +-- two-cycle first hop, in which no instruction is executed, so the simulator +-- gets no leakage, the simulator's driver gives the same hop length as the +-- core's, the two make the same bus observations, and 'simInv' holds +-- afterwards. The register file and memory are arbitrary, as in +-- 'Proof.Functional.Obligation.baseCaseObligation'. +baseCaseLeakObligation :: + forall r m. (RegFileOps r, MemOps m) => r Identity -> m -> Address -> Bool +baseCaseLeakObligation rf mem pc = + simDriver Nothing sim == 1 + && obs1 == obsOf out1 + && obs2 == obsOf out2 + && simInv sim2 sys2 + where + st = (Core.init :: Core.StateG r Identity) {Core.stateFePc = pc, Core.stateRegFile = rf} + sys = Sys st Core.initInput mem + sim = simInit {simStateFePc = pc} + + (sys1, out1) = stepSysOut sys + (sim1, obs1) = simCircuit sim Nothing + + (sys2, out2) = stepSysOut sys1 + (sim2, obs2) = simCircuit sim1 Nothing + +-- | The @k = 0@ leakage step: the one-cycle hop. +-- +-- > inv(isa, sys) /\ simInv(sim, sys) /\ driver(sys) = 0 +-- > ==> simDriver(leak, sim) = 0 /\ obs(sim) = obs(sys) /\ simInv(sim', sys') +-- +-- The simulator gets @leakOf isa@ on the hop's first cycle and nothing after. +indStepLeakObligation :: + (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool +indStepLeakObligation wr wa ipc sys sim = + not premises || conclusion + where + isa = isaAt ipc sys + leak = leakOf isa + + (sys', out') = stepSysOut sys + (sim', obs') = simCircuit sim (Just leak) + + premises = + invAtFree wr wa isa sys + && driver sys == 0 + && simInv sim sys + + conclusion = + simDriver (Just leak) sim == 0 + && obs' == obsOf out' + && simInv sim' sys' + +-- | The @k = 1@ leakage step: the two-cycle hop. +indStepLeakObligation1 :: + (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool +indStepLeakObligation1 wr wa ipc sys sim = + not premises || conclusion + where + isa = isaAt ipc sys + leak = leakOf isa + + (sys1, out1) = stepSysOut sys + (sim1, obs1) = simCircuit sim (Just leak) + + (sys2, out2) = stepSysOut sys1 + (sim2, obs2) = simCircuit sim1 Nothing + + premises = + invAtFree wr wa isa sys + && driver sys == 1 + && simInv sim sys + + conclusion = + simDriver (Just leak) sim == 1 + && obs1 == obsOf out1 + && obs2 == obsOf out2 + && simInv sim2 sys2 + +-- | The @k = 2@ leakage step: the three-cycle hop. +indStepLeakObligation2 :: + (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool +indStepLeakObligation2 wr wa ipc sys sim = + not premises || conclusion + where + isa = isaAt ipc sys + leak = leakOf isa + + (sys1, out1) = stepSysOut sys + (sim1, obs1) = simCircuit sim (Just leak) + + (sys2, out2) = stepSysOut sys1 + (sim2, obs2) = simCircuit sim1 Nothing --- | @proj@ commutes with a driver hop, and the observations agree. -leakObligation :: - (RegFileOps r, MemOps m) => RegIdx -> Address -> SysG r m -> Bool -leakObligation wr wa sys = - not (leakPremises wr wa sys) || (simEq wr (censor sysI) ss' && obsI == obsL) + (sys3, out3) = stepSysOut sys2 + (sim3, obs3) = simCircuit sim2 Nothing + + premises = + invAtFree wr wa isa sys + && driver sys == 2 + && simInv sim sys + + conclusion = + simDriver (Just leak) sim == 2 + && obs1 == obsOf out1 + && obs2 == obsOf out2 + && obs3 == obsOf out3 + && simInv sim3 sys3 + +-- | The @k = 3@ leakage step: the four-cycle hop, the longest. +indStepLeakObligation3 :: + (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool +indStepLeakObligation3 wr wa ipc sys sim = + not premises || conclusion where - (sysI, obsI) = implHop sys - ((_, ss'), obsL) = leakSimHop (proj sys) + isa = isaAt ipc sys + leak = leakOf isa + + (sys1, out1) = stepSysOut sys + (sim1, obs1) = simCircuit sim (Just leak) + + (sys2, out2) = stepSysOut sys1 + (sim2, obs2) = simCircuit sim1 Nothing + + (sys3, out3) = stepSysOut sys2 + (sim3, obs3) = simCircuit sim2 Nothing + + (sys4, out4) = stepSysOut sys3 + (sim4, obs4) = simCircuit sim3 Nothing + + premises = + invAtFree wr wa isa sys + && driver sys == 3 + && simInv sim sys + + conclusion = + simDriver (Just leak) sim == 3 + && obs1 == obsOf out1 + && obs2 == obsOf out2 + && obs3 == obsOf out3 + && obs4 == obsOf out4 + && simInv sim4 sys4 diff --git a/proof/Proof/Leakage/Simulator.hs b/proof/Proof/Leakage/Simulator.hs index 9c790ca..61cf228 100644 --- a/proof/Proof/Leakage/Simulator.hs +++ b/proof/Proof/Leakage/Simulator.hs @@ -1,370 +1,300 @@ --- | The simulator: a machine that sees only the leakage and still reproduces --- everything the attacker can see. +-- | The leakage simulator: a pipeline with the same stage structure and timing +-- as "Core", which sees only the leakage -- never the program, the register +-- file or memory contents. -- --- It is the unmodified 'Core.circuit', run on a censored state and fed --- instruction words made up from the leakage. Per hop: --- --- 1. 'installLeak' puts @'Proof.Leakage.Model.invWord' l@ on the bus. --- 2. 'Proof.Driver.driver' picks the hop length from the censored state, and --- the core runs that many cycles, every instruction fetch answered with --- the same word. --- 3. 'scrub' normalises the state for the next hop. --- --- The hop length is /derived/, not supplied. That is the point: the number of --- cycles an instruction takes is exactly the timing an attacker sees, so a --- simulator that were told it would be proving nothing. --- --- 'proj' is the refinement relation the proof preserves. Its architectural half --- is 'archOfLeak' and its simulator half is 'censor'. +-- Each cycle it may receive the 'Leak' of the instruction entering its execute +-- stage ('SimInput'; 'Nothing' when there is none) and emits the bus +-- observation the core would make that cycle ('SimOutput'). The leakage proof +-- shows that, fed the ISA's leakage, it produces the same observations as the +-- core, so everything an attacker on the bus sees is a function of the leakage +-- alone. module Proof.Leakage.Simulator - ( -- * Simulator states - SimSys, - censor, - censorEx, - censorPast, - exLeak, - installJump, - scrub, - simEq, - - -- * The refinement relation - proj, - archOfLeak, - isaNext, - - -- * The two machines - implHop, - simHop, - leakSimHop, - stepSimOut, - installLeak, + ( SimInput, + SimOutput, + SimExInstrType (..), + SimState (..), + SimControl (..), + SimM, + simCircuit, + simInit, + simInitCtrl, ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) -import Core -import Data.Functor.Identity -import Data.Monoid (getFirst) -import Instruction -import Proof.Driver (driver) -import Proof.Functional.Obligation (hopPc, isStartupShape, isaAt) -import ISA (IsaStateG (..), StepG (..), isaStep) +import Control.Monad +import Control.Monad.RWS +import Data.Maybe (fromMaybe, isJust) +import Instruction (storeHazard) +import Memory.Types import Proof.Leakage.Model -import Memory.Types (MemOps (..)) -import Proof.Machine -import RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) --- Censoring -------------------------------------------------------------------- +-- | The input of the simulator. +type SimInput = Maybe Leak --- | The simulator's state: a core state with the secrets removed. --- --- The memory slot is @()@ -- the simulator has no memory, and answers --- instruction fetches from the leakage and data reads with zero. --- 'Proof.Driver.driver' is polymorphic in the memory type, so it runs on this --- unchanged. -type SimSys r = SysG r () +-- | The output of the simulator. +type SimOutput = Obs --- | Remove the secrets from a core state. --- --- Kept: the three program counters (they are the observable fetch addresses), --- the halt state, the 'Core.inputIsInstr' flag, and the /class/ of each --- pipeline instruction. --- --- Removed: the register file, both result registers, the memory-stage address, --- and the instruction word on the bus. The control lines are reset rather than --- copied, because 'Core.withCtrlReset' rewrites them before any stage reads --- them and they carry nothing between cycles. -censor :: (RegFileOps r) => SysG r m -> SimSys r -censor sys@(Sys st inp _) = - installJump (jumpSource =<< exLeak sys) $ - Sys - { sysState = - State - { stateFePc = stateFePc st, - stateDePc = stateDePc st, - stateExPc = stateExPc st, - stateExInstr = censorEx sys, - stateMeInstr = censorPast (stateMeInstr st), - stateMeRes = Identity 0, - stateMeAddr = 0, - stateWbInstr = censorPast (stateWbInstr st), - stateWbRes = Identity 0, - stateRegFile = initRFg, - stateCtrl = initCtrl, - stateHalt = stateHalt st, - stateHaltNextPc = stateHaltNextPc st - }, - sysInput = Input (inputIsInstr inp) (Identity 0), - sysMem = () - } +data SimExInstrType + = -- | A decoded instruction, whose leakage is the input. + DecodedInstr + | -- | First instruction discarded because of a jump. + StallJumpFirstCycle + | -- | Second instruction discarded because of a jump. + StallJumpSecondCycle + | -- | First instruction discarded because of a load hazard. + StallLoadHazardFirstCycle + | -- | Second instruction discarded because of a load hazard. + StallLoadHazardSecondCycle + | -- | First instruction discarded because of a store hazard. + StallStoreHazardFirstCycle + | -- | Second instruction discarded because of a store hazard. + StallStoreHazardSecondCycle + | -- | No instruction read because of memory bus overload. + StallMemoryBusBusy + | -- | First cycle. + FirstCycle + | -- | The core has halted. + Halted + deriving (Eq, Show, Generic, NFDataX) --- | The leakage of the execute-stage instruction, or 'Nothing' when that stage --- holds a stall @Nop@. --- --- @Nop DecodeFail@ is not a stall: it is what an undecodable memory word --- decodes to, so it is a real architectural instruction and is classified like --- any other non-memory one. 'Proof.Machine.isBubble' draws the same line. -exLeak :: (RegFileOps r) => SysG r m -> Maybe L -exLeak sys = case exInstr sys of - Nop DecodeFail -> Just (L CPlain (Nothing, Nothing)) - Nop _ -> Nothing - ir -> Just (L (coreClass sys ir) (mkDeps ir)) - --- | Censor the execute-stage instruction. --- --- This is the only stage whose instruction still has decisions to make, so it --- is replaced by the representative of its leakage, with the class resolved --- against the /core/ state -- forwarded operands and all. --- --- Stall @Nop@s pass through verbatim: 'Core.decode' reads the reason back off --- @ctrlExInstr@ to decide the follow-on stall, so it is live here. -censorEx :: (RegFileOps r) => SysG r m -> Instruction -censorEx sys = case exLeak sys of - Nothing -> exInstr sys - Just l -> inv l - --- | Censor a memory- or writeback-stage instruction. --- --- These have no decisions left. 'Core.memory' and 'Core.writeback' consult them --- only to decide whether to issue a memory access and of what width, which --- register to forward, and which register to write, so only the memory class --- and width need survive. --- --- The destination register is dropped, unlike in 'censorEx'. No hazard check --- reads it here -- 'Core.decode', 'Proof.Driver.loadHazardD' and the --- invariant's @me->ex@ conjunct all look at the execute stage -- and dropping --- it keeps a censored writeback from clobbering the value 'installJump' parks --- in the register file. With @rd == 0@ the write is a no-op and --- 'Core.regWithFwd' ignores the forwarding line. --- --- Idempotent on its own image, which is what lets 'scrub' apply it to --- instructions the simulator produced itself. -censorPast :: Instruction -> Instruction -censorPast ir = case ir of - Nop DecodeFail -> inv (L CPlain (Nothing, Nothing)) - Nop reason -> Nop reason - IType (Load size _) _ _ _ -> inv (L (CLoad size 0) (mkDeps ir)) - SType size _ _ _ -> inv (L (CStore size) (mkDeps ir)) - _ -> inv (L CPlain (mkDeps ir)) - --- | Park a leaked jump target in the register file, where 'Core.execute' will --- read it back. --- --- The register file is what 'Core.execute' reads, because in a censored state --- neither forwarding line can fire: 'censorPast' gives every memory- and --- writeback-stage instruction @rd == 0@, and 'Core.regWithFwd' ignores @x0@. --- --- The value lives for exactly one hop -- the next 'censor' or 'scrub' rebuilds --- the register file -- and during that hop the only register-reading --- instruction in the execute stage is the @jalr@ that needs it. -installJump :: (RegFileOps r) => Maybe (RegIdx, Address) -> SimSys r -> SimSys r -installJump Nothing ss = ss -installJump (Just (src, target)) (Sys st inp m) = - Sys - st {stateRegFile = modifyRFg src (Identity (pack target)) (stateRegFile st)} - inp - m - --- | Normalise the simulator's state at a hop boundary. --- --- Two jobs. First, discard dead state: the register file, both result --- registers, the memory-stage address and the parked bus word. Every --- instruction 'inv' emits reads only registers held at zero, writes either --- @x0@ or a load result that is zero, and never lets a result value reach an --- observation, so 'censor' can zero them on the implementation side and the --- two still agree. --- --- Second, re-censor the memory- and writeback-stage instructions. 'censorEx' --- resolves an execute-stage branch to a taken or untaken representative, and --- the simulator carries that form down the pipeline; 'censor', looking at the --- implementation one hop later, sees the same instruction in the memory stage --- and cannot recover the outcome, so it uses the plain representative. Running --- 'censorPast' on both sides reconciles them. -scrub :: (RegFileOps r) => L -> SimSys r -> SimSys r -scrub l (Sys st inp _) = - installJump parked $ - Sys - { sysState = - st - { stateMeInstr = censorPast (stateMeInstr st), - stateWbInstr = censorPast (stateWbInstr st), - stateMeRes = Identity 0, - stateWbRes = Identity 0, - stateMeAddr = 0, - stateRegFile = initRFg, - stateCtrl = initCtrl - }, - sysInput = Input (inputIsInstr inp) (Identity 0), - sysMem = () +-- | The internal state of the simulator. +data SimState = SimState + { -- | Program counter fetch stage. + simStateFePc :: Address, + -- | Program counter decode stage. + simStateDePc :: Address, + -- | Does the decode stage expect an instruction? + simStateDeExpInstr :: Bool, + -- | Instruction execute stage. + simStateExInstrType :: SimExInstrType, + -- | Instruction memory stage. + simStateMeInstr :: Leak, + -- | Control/forwarding lines. + simStateCtrl :: SimControl + } + deriving (Eq, Show, Generic, NFDataX) + +-- | Control lines. +data SimControl = SimControl + { -- | Stores `stateDePc` when the instruction in the `decode` stage has + -- a load hazard with the instruction in the `execute` stage. + simCtrlDeLoadHazard :: Maybe Address, + -- | Stores `stateDePc` when the instruction in the `decode` stage has + -- a store hazard with the instruction in the `execute` stage or the + -- instruction in the `memory` stage. + simCtrlDeStoreHazard :: Maybe Address, + -- | Stores the type of instruction in the `execute` stage (if it's a decoded + -- instruction versus various stalls). + simCtrlExInstrType :: Maybe SimExInstrType, + -- | `True` when the leaked instruction is an environment instruction. To + -- maintain consistency with the core, the execute stage is the only one + -- that examines the input, which is why this control line is needed. + simCtrlExEnvInstr :: Bool, + -- | Stores the jump address if the instruction in the `execute` stage + -- results in a jump. + simCtrlExJumpAddr :: Maybe Address, + -- | Stores the write address and size if the instruction in the `execute` stage + -- is a store. + simCtrlExStoreAddrSize :: Maybe (Address, Size), + -- | Stores the load hazard bit if the instruction in the `execute` stage + -- is a load. + simCtrlExLoadHazard :: Maybe Bool, + -- | `True` when the instruction in the `memory` stage is a store or a load. + simCtrlMeMemInstr :: Bool, + -- | Stores the write address and size if the instruction in the `memory` stage + -- is a store. + simCtrlMeStoreAddrSize :: Maybe (Address, Size) + } + deriving (Eq, Show, Generic, NFDataX) + +type SimM = RWS SimInput SimOutput SimState + +simSetLines :: (SimControl -> SimControl) -> SimM () +simSetLines f = modify $ \s -> s {simStateCtrl = f (simStateCtrl s)} + +-- | Run the simulator for one step. +simCircuit :: SimState -> SimInput -> (SimState, SimOutput) +simCircuit = flip $ execRWS simPipe + +-- | The simulator, composed of each stage. +simPipe :: SimM () +simPipe = do + -- The control lines need to be reset every tick. + modify $ \s -> s {simStateCtrl = simInitCtrl} + simWriteback + simMemory + simExecute + simDecode + simFetch + +simInit :: SimState +simInit = + SimState + { simStateFePc = initPc, + simStateDePc = 0, + simStateDeExpInstr = False, + simStateExInstrType = FirstCycle, + simStateMeInstr = LArith, + simStateCtrl = simInitCtrl + } + +-- | Initial control lines. +simInitCtrl :: SimControl +simInitCtrl = + SimControl + { simCtrlDeLoadHazard = Nothing, + simCtrlDeStoreHazard = Nothing, + simCtrlExInstrType = Nothing, + simCtrlExEnvInstr = False, + simCtrlExJumpAddr = Nothing, + simCtrlExStoreAddrSize = Nothing, + simCtrlExLoadHazard = Nothing, + simCtrlMeMemInstr = False, + simCtrlMeStoreAddrSize = Nothing + } + +-- | Fetch stage. +simFetch :: SimM () +simFetch = do + pc <- gets simStateFePc + ctrl <- gets simStateCtrl + + -- We stall if the instruction in the `memory` stage is a load or a store. + let stall = simCtrlMeMemInstr ctrl + + -- Always try to read unless we stall. + unless stall $ + simReadPC pc + + let next_pc = + fromMaybe + (fromMaybe + (fromMaybe + (if stall then pc else pc + 4) + (simCtrlDeLoadHazard ctrl)) + (simCtrlDeStoreHazard ctrl)) + (simCtrlExJumpAddr ctrl) + + modify $ \s -> + s { -- Increment program counter for next fetch. + simStateFePc = next_pc, + -- Propagate program counter to next stage. + simStateDePc = pc, + -- Decode expects an instruction next cycle iff we fetch now. + simStateDeExpInstr = not stall } - where - -- The instruction that just reached the execute stage is the one this hop - -- injected, so its leakage is @l@ -- unless it was squashed or the core - -- halted, in which case that stage holds a @Nop@ and nothing is parked. - parked - | stateExInstr st == inv l = jumpSource l - | otherwise = Nothing - --- | Structural equality on simulator states, at one witness register. --- --- 'SysG' has an 'Eq' instance, but it needs @'Eq' (r 'Identity')@, which the --- SMT-array register file does not have; the register file is compared --- pointwise instead, as 'Proof.Functional.Invariant.invAtFree' does. Quantifying --- over the witness recovers full equality. --- --- The control lines are not compared: 'Core.withCtrlReset' resets them at the --- start of every cycle, so they carry nothing between hops. -simEq :: (RegFileOps r) => RegIdx -> SimSys r -> SimSys r -> Bool -simEq wr (Sys a ia _) (Sys b ib _) = - stateFePc a == stateFePc b - && stateDePc a == stateDePc b - && stateExPc a == stateExPc b - && stateExInstr a == stateExInstr b - && stateMeInstr a == stateMeInstr b - && stateMeAddr a == stateMeAddr b - && stateWbInstr a == stateWbInstr b - && runIdentity (stateMeRes a) == runIdentity (stateMeRes b) - && runIdentity (stateWbRes a) == runIdentity (stateWbRes b) - && stateHalt a == stateHalt b - && stateHaltNextPc a == stateHaltNextPc b - && inputIsInstr ia == inputIsInstr ib - && runIdentity (lookupRFg wr (stateRegFile a)) == runIdentity (lookupRFg wr (stateRegFile b)) - && runIdentity (inputMem ia) == runIdentity (inputMem ib) - --- The refinement relation ------------------------------------------------------ - --- | 'isaStep' made total: a halted ISA stands still. -isaNext :: (RegFileOps r, MemOps m) => IsaStateG r m -> IsaStateG r m -isaNext a = case isaStep a of - Next a' -> a' - IsaHalted -> a - --- | The architectural state a core state corresponds to, for the leakage proof. --- --- Fetch-aligned: the instruction at its PC is the one the pipeline is /taking --- in/, not the one in the execute stage. 'Proof.Functional.Obligation.hopPc' --- is execute-aligned, one instruction behind, so a single --- 'isaStep' converts between them. --- --- The alignment is forced. The simulator's only channel into the core is the --- instruction word on the bus, and the invariant pins that word to --- @mem[dePc] == mem[isaPc + 4]@ -- the instruction after the one in execute. So --- the leakage a hop consumes must describe that one. --- --- At reset nothing is in flight and the PC comes off the fetch stage, exactly as --- 'Proof.Functional.Obligation.hopPc' already does there. -archOfLeak :: (RegFileOps r, MemOps m) => SysG r m -> IsaStateG r m -archOfLeak sys - | isStartupShape sys = isaAt (hopPc sys) sys - | otherwise = isaNext (isaAt (hopPc sys) sys) --- | The refinement relation: an architectural state paired with a censored core. -proj :: (RegFileOps r, MemOps m) => SysG r m -> (IsaStateG r m, SimSys r) -proj sys = (archOfLeak sys, censor sys) +-- | Decode stage. +simDecode :: SimM () +simDecode = do + pc <- gets simStateDePc + expInstr <- gets simStateDeExpInstr + ctrl <- gets simStateCtrl --- The two machines ------------------------------------------------------------- + let irt = if expInstr then DecodedInstr else StallMemoryBusBusy --- | One simulator cycle. --- --- The shape of 'Proof.Machine.stepSysOut', except that there is no memory to --- service: an instruction fetch is answered with the leaked word, a data read --- with zero, and a write with zero exactly as 'Proof.Machine.stepSys' does. -stepSimOut :: (RegFileOps r) => Word -> SimSys r -> (SimSys r, Output Identity) -stepSimOut w (Sys s i _) = - let (s', o) = Core.circuit s i - i' = case getFirst (outMem o) of - Just (MemAccess isInstr _ _ Nothing) -> - Input isInstr (Identity (if isInstr then w else 0)) - Just (MemAccess isInstr _ _ (Just _)) -> Input isInstr (Identity 0) - Nothing -> Input False (Identity 0) - in (Sys s' i' (), o) - --- | Put the leaked instruction word on the simulator's bus. --- --- Only onto an instruction fetch. When 'Core.inputIsInstr' is 'False' the bus --- carries the data for a load in the writeback stage, and 'Core.writeback' --- would sign-extend the instruction word into a register. The censored value --- there is zero and stays zero; the leaked word reaches 'Core.decode' one cycle --- later through 'stepSimOut'. -installLeak :: Word -> SimSys r -> SimSys r -installLeak word (Sys s i m) - | inputIsInstr i = Sys s (Input True (Identity word)) m - | otherwise = Sys s i m - --- | The implementation, run for one driver hop, with the observation of each --- cycle. --- --- A four-way case rather than a loop: @driver sys@ is symbolic and Pantomime --- cannot unroll a symbolic count. -implHop :: (RegFileOps r, MemOps m) => SysG r m -> (SysG r m, HopObs) -implHop sys = case driver sys of - 0 -> - let (s1, o1) = stepSysOut sys - in (s1, HopObs (Just (obsOf o1)) Nothing Nothing Nothing) - 1 -> - let (s1, o1) = stepSysOut sys - (s2, o2) = stepSysOut s1 - in (s2, HopObs (Just (obsOf o1)) (Just (obsOf o2)) Nothing Nothing) - 2 -> - let (s1, o1) = stepSysOut sys - (s2, o2) = stepSysOut s1 - (s3, o3) = stepSysOut s2 - in (s3, HopObs (Just (obsOf o1)) (Just (obsOf o2)) (Just (obsOf o3)) Nothing) - _ -> - let (s1, o1) = stepSysOut sys - (s2, o2) = stepSysOut s1 - (s3, o3) = stepSysOut s2 - (s4, o4) = stepSysOut s3 - in (s4, HopObs (Just (obsOf o1)) (Just (obsOf o2)) (Just (obsOf o3)) (Just (obsOf o4))) - --- | The simulator, run for one hop. --- --- The leaked word goes on the bus before the hop length is asked for, because --- 'Proof.Driver.driver' reads it: a load-use hazard between the incoming --- instruction and a load in the execute stage is one of the things that decides --- how long the hop is. -simHop :: (RegFileOps r) => SimSys r -> L -> (SimSys r, HopObs) -simHop ss l = (scrub l ss', o) - where - w = invWord l - ss0 = installLeak w ss - (ss', o) = case driver ss0 of - 0 -> - let (s1, o1) = stepSimOut w ss0 - in (s1, HopObs (Just (obsOf o1)) Nothing Nothing Nothing) - 1 -> - let (s1, o1) = stepSimOut w ss0 - (s2, o2) = stepSimOut w s1 - in (s2, HopObs (Just (obsOf o1)) (Just (obsOf o2)) Nothing Nothing) - 2 -> - let (s1, o1) = stepSimOut w ss0 - (s2, o2) = stepSimOut w s1 - (s3, o3) = stepSimOut w s2 - in (s3, HopObs (Just (obsOf o1)) (Just (obsOf o2)) (Just (obsOf o3)) Nothing) - _ -> - let (s1, o1) = stepSimOut w ss0 - (s2, o2) = stepSimOut w s1 - (s3, o3) = stepSimOut w s2 - (s4, o4) = stepSimOut w s3 - in (s4, HopObs (Just (obsOf o1)) (Just (obsOf o2)) (Just (obsOf o3)) (Just (obsOf o4))) - --- | Specification and simulator, composed. --- --- The architectural state steps, and the simulator is handed the leakage of the --- instruction that state is currently processing. Nothing here mentions the --- pipeline: the leakage is @'leakOf' a@, a function of the architectural state --- alone. That is the point of the construction -- an attacker model that can be --- stated without the processor in it. --- --- A closed machine, unlike its counterpart in the @highlevel-leakage@ --- development: AIMCore's ISA reads its instruction out of its own memory, so --- the architectural state is all the input there is. -leakSimHop :: - (RegFileOps r, MemOps m) => - (IsaStateG r m, SimSys r) -> - ((IsaStateG r m, SimSys r), HopObs) -leakSimHop (a, ss) = ((isaNext a, ss'), o) - where - (ss', o) = simHop ss (leakOf a) + let halted = simCtrlExInstrType ctrl == Just Halted + let env_instr_current_cycle = simCtrlExEnvInstr ctrl + + let jump_previous_cycle = simCtrlExInstrType ctrl == Just StallJumpFirstCycle + let store_hazard_previous_cycle = simCtrlExInstrType ctrl == Just StallStoreHazardFirstCycle + let load_hazard_previous_cycle = simCtrlExInstrType ctrl == Just StallLoadHazardFirstCycle + + let jump_current_cycle = isJust (simCtrlExJumpAddr ctrl) + + let store_hazard_current_cycle = + maybe False (storeHazard pc) (simCtrlExStoreAddrSize ctrl) || + maybe False (storeHazard pc) (simCtrlMeStoreAddrSize ctrl) + + let load_hazard_current_cycle = expInstr && fromMaybe False (simCtrlExLoadHazard ctrl) + + let irt' + -- Halt if the core is not running anymore. + | halted = Halted + -- Halt if there is an environment instruction in this cycle. + | env_instr_current_cycle = Halted + -- Stall if there was a jump in the previous cycle. + | jump_previous_cycle = StallJumpSecondCycle + -- Stall if there was a store hazard in the previous cycle. + | store_hazard_previous_cycle = StallStoreHazardSecondCycle + -- Stall if there was a load hazard in the previous cycle. + | load_hazard_previous_cycle = StallLoadHazardSecondCycle + -- Stall if there is a jump in this cycle. + | jump_current_cycle = StallJumpFirstCycle + -- Stall if there is a store hazard in this cycle. + | store_hazard_current_cycle = StallStoreHazardFirstCycle + -- Stall if there is a load hazard in this cycle. + | load_hazard_current_cycle = StallLoadHazardFirstCycle + -- Otherwise we process the decoded instruction. + | otherwise = irt + + modify $ \s -> s {simStateExInstrType = irt'} + + when (irt' == StallStoreHazardFirstCycle) $ do + simSetLines $ \c -> c {simCtrlDeStoreHazard = Just pc} + + when (irt' == StallLoadHazardFirstCycle) $ do + simSetLines $ \c -> c {simCtrlDeLoadHazard = Just pc} + +-- | Execute stage. +simExecute :: SimM () +simExecute = do + input <- ask + irt <- gets simStateExInstrType + + simSetLines $ \c -> c {simCtrlExInstrType = Just irt} + + case irt of + DecodedInstr -> + case input of + Just ir -> do + modify $ \s -> s {simStateMeInstr = ir} + + case ir of + LArith -> pure () + LJump addr -> + simSetLines $ \c -> c {simCtrlExJumpAddr = Just addr} + LLoad _ _ haz -> + simSetLines $ \c -> c {simCtrlExLoadHazard = Just haz} + LStore size addr -> + simSetLines $ \c -> c {simCtrlExStoreAddrSize = Just (addr, size)} + LEnv -> + simSetLines $ \c -> c {simCtrlExEnvInstr = True} + Nothing -> modify $ \s -> s {simStateMeInstr = LArith} + _ -> modify $ \s -> s {simStateMeInstr = LArith} + +-- | Memory stage. +simMemory :: SimM () +simMemory = do + ir <- gets simStateMeInstr + + case ir of + LArith -> pure () + LJump _ -> pure () + LLoad size addr _ -> do + simSetLines $ \c -> c {simCtrlMeMemInstr = True} + simReadRAM addr size + LStore size addr -> do + simSetLines $ \c -> + c {simCtrlMeMemInstr = True, simCtrlMeStoreAddrSize = Just (addr, size)} + simWriteRAM addr size + LEnv -> pure () + +-- | Writeback stage. +simWriteback :: SimM () +simWriteback = pure () + +simReadPC :: Address -> SimM () +simReadPC addr = + tell $ Fetch addr + +simReadRAM :: Address -> Size -> SimM () +simReadRAM addr size = + tell $ DataRead addr size + +simWriteRAM :: Address -> Size -> SimM () +simWriteRAM addr size = + tell $ DataWrite addr size From 5b7e3dd6e4295d3344eb279dbebd2c034a028e44 Mon Sep 17 00:00:00 2001 From: Kristina Date: Fri, 9 Oct 2026 23:43:53 +0200 Subject: [PATCH 4/8] Update the build and tests for the new core and proofs package.yaml lists the moved and new modules: Proof.Functional.Driver, the leakage Driver and Invariant, and, behind the smt-proof flag, the SMT helpers, Proof.SMT.System and Proof.Leakage.Induction. Tests: - Generators and hand-built states set stateDeExpInstr instead of an input flag, and use stateExPc / stateHalt where they used hopPc, exInstr and running. - Spec checks the leakage base case and the four leakage steps alongside the functional ones, and InstructionSpec tests isMemInstr. - ProofSpec gains leakReport, the concrete counterpart of the leakage induction: the simulator runs alongside the core hop by hop, and every hop must have the same length in both, the same bus observation every cycle, and simInv afterwards. It passes on the fixed programs and 2000 random ones, so the leakage steps' premises hold on reachable states. - Unused getFirst imports left over from the removed outSyscall field are dropped. The full build with the smt-proof flag passes all symbolic properties and the test suite. Co-Authored-By: Claude Opus 5.5 --- package.yaml | 17 +++-- test/BenchmarkSpec.hs | 1 - test/InstructionSpec.hs | 8 ++- test/ProofSpec.hs | 156 ++++++++++++++++++++++++++++++---------- test/Spec.hs | 37 ++++++---- 5 files changed, 156 insertions(+), 63 deletions(-) diff --git a/package.yaml b/package.yaml index bca72b4..cbf1871 100644 --- a/package.yaml +++ b/package.yaml @@ -110,24 +110,23 @@ library: source-dirs: proof-smt exposed-modules: - Proof.Functional.Induction + - Proof.Leakage.Induction + - Proof.SMT.Array + - Proof.SMT.Axioms + - Proof.SMT.Logged - Proof.SMT.Sanity + - Proof.SMT.System cpp-options: -DSMT_PROOF exposed-modules: - Proof.Machine - - Proof.Driver + - Proof.Functional.Driver - Proof.Functional.Invariant - Proof.Functional.Obligation - Proof.Leakage.Model - Proof.Leakage.Simulator + - Proof.Leakage.Driver + - Proof.Leakage.Invariant - Proof.Leakage.Obligation - # Proof.Leakage.Induction: temporarily out of the build. Its four properties - # are invalid since the aliasing-store assumption was dropped, and the - # counterexample-extraction path trips a Pantomime/effectful unlifting bug - # ("version (2356) /= storageVersion (0)") that fails the build outright. - # Restore once the leakage model can express the store-hazard stall. - - Proof.SMT.Array - - Proof.SMT.Axioms - - Proof.SMT.Logged - Access - Core - Elf.ElfLoader diff --git a/test/BenchmarkSpec.hs b/test/BenchmarkSpec.hs index b77f123..df15b85 100644 --- a/test/BenchmarkSpec.hs +++ b/test/BenchmarkSpec.hs @@ -13,7 +13,6 @@ import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.ST (stToIO, RealWorld) import qualified Core as Core import Data.Functor.Identity -import Data.Monoid (First (getFirst)) import Elf.ElfLoader import Elf.Syscall (handleSyscall) import Numeric (showHex) diff --git a/test/InstructionSpec.hs b/test/InstructionSpec.hs index de82617..3d7f46a 100644 --- a/test/InstructionSpec.hs +++ b/test/InstructionSpec.hs @@ -224,10 +224,12 @@ testInstructionPredicates = testGroup "Instruction Predicates" isCall callInstr @?= True isCall nop @?= False, - testCase "isLoad predicate" $ do + testCase "isMemInstr predicate" $ do let loadInstr = IType (Load Word Signed) 1 2 100 - isLoad loadInstr @?= True - isLoad nop @?= False + storeInstr = SType Word 100 1 2 + isMemInstr loadInstr @?= True + isMemInstr storeInstr @?= True + isMemInstr nop @?= False ] -- | Test register extraction functions diff --git a/test/ProofSpec.hs b/test/ProofSpec.hs index 2060161..c258f60 100644 --- a/test/ProofSpec.hs +++ b/test/ProofSpec.hs @@ -6,12 +6,16 @@ import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Clash.Sized.Vector (unsafeFromList) import Core import Data.Functor.Identity (Identity (..), runIdentity) -import Proof.Driver +import Proof.Functional.Driver hiding (loadHazard, storeHazard) import ISA (IsaStateG (..), IsaState, StepG (..), isaStep, isaInstrAt) import Instruction import Proof.Functional.Invariant import Proof.Machine -import Proof.Functional.Obligation (indStepObligation, indStepObligation1, indStepObligation2, hopPc, isaAt) +import Proof.Functional.Obligation (indStepObligation, indStepObligation1, indStepObligation2, isaAt) +import Proof.Leakage.Driver (simDriver) +import Proof.Leakage.Invariant (simInv) +import Proof.Leakage.Model (Obs, leakOf, obsOf) +import Proof.Leakage.Simulator (SimInput, SimState, simCircuit, simInit) import Memory.Types import RegFile import Test.Tasty (TestTree, testGroup) @@ -28,7 +32,7 @@ import qualified Prelude as P -- driver has an explicit case for. Note @Nop DecodeFail@ is /not/ a bubble -- -- see 'Proof.Machine.isBubble'. aligned :: Sys -> Bool -aligned s = not (isBubble (exInstr s)) || exInstr s == Nop FirstCycle +aligned s = not (isBubble (stateExInstr (sysState s))) || stateExInstr (sysState s) == Nop FirstCycle -- | Walk the machine from aligned state to aligned state, taking -- @driver s + 1@ cycles each hop. @@ -39,7 +43,7 @@ alignedWalk k prog = go k 0 (initSys prog) go j i s = let n = driver s + 1 s' = stepSysN n s - in (i, n, s') : if running s' then go (j - 1) (i + n) s' else [] + in (i, n, s') : if stateHalt (sysState s') == Nothing then go (j - 1) (i + n) s' else [] -- | Hops that do not land on an aligned state. walkReport :: Int -> Vec PROG_SIZE Word -> String @@ -51,13 +55,13 @@ walkReport k prog = " took ", show n, " cycles -> ex=", - show (exInstr s'), + show (stateExInstr (sysState s')), " exPc=", show (stateExPc (sysState s')) ] | (i, n, s') <- alignedWalk k prog, not (aligned s'), - running s' + stateHalt (sysState s') == Nothing ] -- | The architectural state @prog@ starts in: execution begins at 'initPc', the @@ -110,7 +114,7 @@ invTrace k prog = go k 0 isa0 sys0 True IsaHalted -> [(c', isa, sys')] Next isa' -> (c', isa', sys') - : if running sys' then go (j - 1) c' isa' sys' False else [] + : if stateHalt (sysState sys') == Nothing then go (j - 1) c' isa' sys' False else [] -- | The first point at which the invariant fails, with an explanation. invReport :: Int -> Vec PROG_SIZE Word -> String @@ -126,7 +130,7 @@ invReport k prog = " isaInstr=", show (isaInstrAt isa), "\n ex=", - show (exInstr sys), + show (stateExInstr (sysState sys)), " exPc=", show (stateExPc (sysState sys)), " me=", @@ -139,6 +143,63 @@ invReport k prog = explain isa sys ] +-- | The leakage simulator run alongside the core, hop by hop, on a concrete +-- program. Returns the first discrepancy, or @""@ if there is none. +-- +-- The concrete counterpart of "Proof.Leakage.Induction", in the way 'invTrace' +-- is of the functional one. Both machines start from their initial states and +-- take the first hop with no leakage, as in the leakage base case. After that, +-- each hop feeds the simulator @'leakOf' isa@ on its first cycle and nothing +-- after, and the ISA takes one step. At every hop the two drivers must agree on +-- the length, every cycle's bus observation must match, and 'simInv' must hold +-- at the end. +-- +-- It runs on the real 'Vec'-backed state, so it does not rely on the trusted +-- array and term axioms the symbolic proof uses. It also shows that the +-- leakage steps' premises hold on states the machines actually reach. +leakReport :: Int -> Vec PROG_SIZE Word -> String +leakReport k prog = + case checkHop 0 (driver sys0) (simDriver Nothing simInit) firstHop of + Just problem -> "first hop: " P.++ problem + Nothing -> go k (driver sys0 + 1) (initIsa prog) sysAfter simAfter + where + sys0 = initSys prog + firstHop@(sysAfter, simAfter, _, _) = runHop (driver sys0 + 1) sys0 simInit Nothing + + go :: Int -> Int -> IsaState -> Sys -> SimState -> String + go 0 _ _ _ _ = "" + go j c isa sys sim = + let leak = leakOf isa + n = driver sys + 1 + result@(sys', sim', _, _) = runHop n sys sim (Just leak) + in case checkHop c (driver sys) (simDriver (Just leak) sim) result of + Just problem -> problem P.++ "\n isaPc=" P.++ show (isaPc isa) P.++ " leak=" P.++ show leak + Nothing -> case isaStep isa of + IsaHalted -> "" + Next isa' + | stateHalt (sysState sys') == Nothing -> go (j - 1) (c + n) isa' sys' sim' + | otherwise -> "" + + -- Both machines for @n@ cycles; the simulator gets @inp@ on the first only. + runHop :: Int -> Sys -> SimState -> SimInput -> (Sys, SimState, [Obs], [Obs]) + runHop n sys sim inp = loop n sys sim inp [] [] + where + loop 0 s m _ cs ms = (s, m, P.reverse cs, P.reverse ms) + loop j s m i cs ms = + let (s', o) = stepSysOut s + (m', ob) = simCircuit m i + in loop (j - 1) s' m' Nothing (obsOf o : cs) (ob : ms) + + checkHop :: Int -> Int -> Int -> (Sys, SimState, [Obs], [Obs]) -> Maybe String + checkHop c coreK simK (sys', sim', coreObs, simObs) + | coreK /= simK = + Just ("hop at cycle " P.++ show c P.++ ": driver says " P.++ show coreK P.++ ", simDriver says " P.++ show simK) + | ((i, co, so) : _) <- [x | x@(_, co, so) <- P.zip3 [c ..] coreObs simObs, co /= so] = + Just ("observations differ at cycle " P.++ show i P.++ ": core " P.++ show co P.++ ", simulator " P.++ show so) + | P.not (simInv sim' sys') = + Just ("simInv fails after the hop starting at cycle " P.++ show c P.++ "\n sim=" P.++ show sim') + | otherwise = Nothing + progs :: [(String, Vec PROG_SIZE Word)] progs = [ ("prog1 (arith+store)", mkProg prog1), @@ -282,16 +343,30 @@ proofTests = -- is no next non-bubble for the operational reading to find. testCase "driver agrees with its operational reading" $ let bad = - [ (driver sys, ref, exInstr sys) + [ (driver sys, ref, stateExInstr (sysState sys)) | prog <- allProgs 500, (_, _, sys) <- invTrace 40 prog, - running sys, + stateHalt (sysState sys) == Nothing, aligned sys, - P.not (isEnvInstr (exInstr sys)), + P.not (isEnvInstr (stateExInstr (sysState sys))), let ref = driverRef 12 sys, ref /= Just (driver sys + 1) ] in if P.null bad then pure () else assertFailure (show (P.take 10 bad)), + -- The leakage simulator alongside the core: matching hop lengths and bus + -- observations, and 'simInv' after every hop. See 'leakReport'. + testGroup + "simulator matches the core along the driven walk" + [ testCase name $ + let r = leakReport 40 prog + in if P.null r then pure () else assertFailure ("\n" P.++ r) + | (name, prog) <- progs + ], + testProperty "simulator matches the core on random programs" $ + withMaxSuccess 2000 $ + forAll genProg $ \prog -> + let r = leakReport 40 prog + in counterexample (show prog P.++ "\n" P.++ r) (P.null r), testProperty "driver and invariant on random programs" $ withMaxSuccess 2000 $ forAll genProg $ \prog -> @@ -384,12 +459,12 @@ proofTests = in counterexample ( "me=" P.++ show (stateMeInstr (sysState sys)) P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (exInstr sys) + P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa P.++ "\nfailing=" P.++ show (P.map P.fst (P.filter (P.not . P.snd) (P.concatMap caseConjuncts (invCasesAt wr wa isa' sys')))) ) - (indStepObligation wr wa (hopPc sys) sys), + (indStepObligation wr wa (stateExPc (sysState sys)) sys), -- k = 1: the two-cycle hop, a memory instruction in writeback. The test -- below asserts generated states actually satisfy the premise, since one -- this specific is easy to miss entirely and still see a green property. @@ -403,20 +478,20 @@ proofTests = in counterexample ( "me=" P.++ show (stateMeInstr (sysState sys)) P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (exInstr sys) + P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) P.++ " fePc=" P.++ show (stateFePc (sysState sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa P.++ "\nfailing=" P.++ show (P.map P.fst (P.filter (P.not . P.snd) (P.concatMap caseConjuncts (invCasesAt wr wa isa' s2)))) ) - (indStepObligation1 wr wa (hopPc sys) sys), + (indStepObligation1 wr wa (stateExPc (sysState sys)) sys), testCase "k=1 generator satisfies the premise" $ let sample = [s | (s, _, _) <- unGen (vectorOf 4000 genArbSys1) (mkQCGen 7) 30] admitted = [ () | s <- sample, driver s P.== 1, - invAtFree 1 0 (isaAt (hopPc s) s) s + invAtFree 1 0 (isaAt (stateExPc (sysState s)) s) s ] in assertBool "no generated state satisfied the k=1 premise" (P.not (P.null admitted)), -- k = 2: jumps and the all-memory steady shape return to a running @@ -430,18 +505,18 @@ proofTests = P.++ " driverCase=" P.++ driverCaseName sys P.++ "\nme=" P.++ show (stateMeInstr (sysState sys)) P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (exInstr sys) + P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa ) - (indStepObligation2 wr wa (hopPc sys) sys), + (indStepObligation2 wr wa (stateExPc (sysState sys)) sys), testCase "k=2 generator reaches env, jump, and steady cases" $ let sample = [ (label, driverCaseName s) | (label, s, wr, wa) <- unGen (vectorOf 4000 genArbSys2) (mkQCGen 29) 30, driver s P.== 2, - invAtFree wr wa (isaAt (hopPc s) s) s + invAtFree wr wa (isaAt (stateExPc (sysState s)) s) s ] has label = P.any ((P.== label) . P.fst) sample in do @@ -471,7 +546,7 @@ proofTests = -- invariant claims it corresponds to. -- Shared with 'Proof.Functional.Induction.indStep0' via "Proof.Functional.Obligation", so the two cannot drift. isaFromSys :: (RegFileOps r, MemOps m) => SysG r m -> IsaStateG r m -isaFromSys sys = isaAt (hopPc sys) sys +isaFromSys sys = isaAt (stateExPc (sysState sys)) sys -- | Take one driven step and report whether the invariant survived. Returns -- 'Nothing' when @sys@ does not satisfy the invariant to begin with (such a @@ -496,9 +571,9 @@ sampleStates n = [ sys | prog <- allProgs n, (_, _, sys) <- invTrace 40 prog, - running sys, + stateHalt (sysState sys) == Nothing, aligned sys, - P.not (isEnvInstr (exInstr sys)) + P.not (isEnvInstr (stateExInstr (sysState sys))) ] -- | Put a jump in the memory stage. The invariant permits this -- a jump is not @@ -555,6 +630,7 @@ wrapCESys = ( (sysState (initSys (mkProg prog1))) { stateFePc = 0x00000000, stateDePc = 0xFFFFFFFC, + stateDeExpInstr = True, stateExPc = 0xFFFFFFF8, stateExInstr = decode' wrapExWord, -- The store's address and value live in stateMeAddr / stateMeRes; @@ -571,7 +647,7 @@ wrapCESys = stateHaltNextPc = 0 } ) - (Input True (pure wrapDeWord)) + (Input (pure wrapDeWord)) wrapMem -- Arbitrary-state search ------------------------------------------------------ @@ -585,9 +661,9 @@ wrapCESys = -- construction (PCs three words apart, ex latched from mem[exPc], inputMem -- from mem[dePc]) so the premise is not discarded; everything else is random. -- --- 'stateCtrl' is left at 'initCtrl' soundly: 'Core.pipe' is wrapped in --- 'Core.withCtrlReset', which overwrites it before any stage reads it, so the --- incoming value cannot affect 'Proof.Machine.stepSys'. +-- 'stateCtrl' is left at 'initCtrl' soundly: 'Core.pipe' overwrites it at the +-- start of the cycle, before any stage reads it, so the incoming value cannot +-- affect 'Proof.Machine.stepSys'. -- | Instruction generators that build in the premise's constraints, rather than -- generating freely and filtering. Filtering discarded ~6 examples per hit, @@ -701,8 +777,8 @@ genFn gk gv gd = do -- from mem[dePc], writeback non-memory, execute neither environment nor jump, -- no load-use hazard, no halt in flight. -- --- 'stateCtrl' is left at 'initCtrl' soundly: 'Core.pipe' is wrapped in --- 'Core.withCtrlReset', which overwrites it before any stage reads it. +-- 'stateCtrl' is left at 'initCtrl' soundly: 'Core.pipe' overwrites it at the +-- start of the cycle, before any stage reads it. genArbSys :: Gen (SysG RegFn MemFn, RegIdx, Address) genArbSys = do -- Occasionally sit the pipeline astride the top of the address space: the @@ -756,6 +832,7 @@ genArbSys = do ((sysState (initSys (mkProg prog1))) { stateFePc = base + 8, stateDePc = base + 4, + stateDeExpInstr = True, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -768,7 +845,7 @@ genArbSys = do stateHalt = Nothing, stateHaltNextPc = 0 }) - (Input True (pure w1)) + (Input (pure w1)) (MemFn memf) P.pure (sys, wr, wa) @@ -830,7 +907,7 @@ genRunning2 label genEx = do -- premise is exercised rather than making those samples vacuous. let ma = base + 64 wbMem = isMemInstr wbI - inp = if wbMem then Input False (pure loaded) else Input True (pure w1) + inp = Input (pure (if wbMem then loaded else w1)) fePc = if wbMem then base + 4 else base + 8 wr <- genWitnessReg wa <- unpack <$> genW @@ -839,6 +916,7 @@ genRunning2 label genEx = do ( (sysState (initSys (mkProg prog1))) { stateFePc = fePc, stateDePc = base + 4, + stateDeExpInstr = P.not wbMem, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -899,6 +977,7 @@ genSteady2 = do ( (sysState (initSys (mkProg prog1))) { stateFePc = base + 4, stateDePc = base + 4, + stateDeExpInstr = False, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -912,7 +991,7 @@ genSteady2 = do stateHaltNextPc = 0 } ) - (Input False (pure loaded)) + (Input (pure loaded)) (MemFn memf) P.pure ("steady", sys, wr, wa) @@ -943,6 +1022,7 @@ genSteady1 = do ( (sysState (initSys (mkProg prog1))) { stateFePc = base + 4, stateDePc = base + 4, + stateDeExpInstr = False, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -956,7 +1036,7 @@ genSteady1 = do stateHaltNextPc = 0 } ) - (Input False (pure loaded)) + (Input (pure loaded)) (MemFn memf) P.pure (sys, wr, wa) @@ -1152,8 +1232,8 @@ genTakenTransfer useJalr = do let target = base + delta w1 = P.maybe 0 P.id (encode' (roundTrips nextI)) wT = P.maybe 0 P.id (encode' (roundTrips tgtI)) - wbMem = isLoad wbI || isStore wbI - inp = if wbMem then Input False (pure loaded) else Input True (pure w1) + wbMem = isMemInstr wbI + inp = Input (pure (if wbMem then loaded else w1)) fePc = if wbMem then base + 4 else base + 8 ma = base + 4096 -- parked away from every PC and from the target @@ -1162,6 +1242,7 @@ genTakenTransfer useJalr = do ( (sysState (initSys (mkProg prog1))) { stateFePc = fePc, stateDePc = base + 4, + stateDeExpInstr = P.not wbMem, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -1184,7 +1265,7 @@ genTakenTransfer useJalr = do | a - target P.< 4 = byteAt wT (a - target) | P.otherwise = 0 - -- Probe the forwarded operands; 'Proof.Driver.exArg' never reads the execute + -- Probe the forwarded operands; 'Proof.Functional.Driver.exArg' never reads the execute -- stage, so a provisional instruction there makes the probe exact. let probe = mkSys 0 rfF v1 = exArg probe rs1 @@ -1236,7 +1317,7 @@ genLoadHazard3 = do P.pure (IType (Env Break) 0 rd 1) ] meI <- suchThat genStageInstr (\m -> P.not (loadHazard exI m)) - wbI <- suchThat genStageInstr (\i -> P.not (isLoad i || isStore i)) + wbI <- suchThat genStageInstr (P.not . isMemInstr) mk3 base exI meI wbI nextI False genAllMem3 :: Gen (SysG RegFn MemFn, RegIdx, Address) @@ -1276,6 +1357,7 @@ mk3 base exI meI wbI nextI wbMem = do ( (sysState (initSys (mkProg prog1))) { stateFePc = if wbMem then base + 4 else base + 8, stateDePc = base + 4, + stateDeExpInstr = P.not wbMem, stateExPc = base, stateExInstr = decode' w0, stateMeInstr = meI, @@ -1289,7 +1371,7 @@ mk3 base exI meI wbI nextI wbMem = do stateHaltNextPc = 0 } ) - (if wbMem then Input False (pure loaded) else Input True (pure w1)) + (Input (pure (if wbMem then loaded else w1))) (MemFn memf), wr, wa diff --git a/test/Spec.hs b/test/Spec.hs index 163a095..92993a7 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -28,6 +28,7 @@ import qualified Proof.SMT.Sanity as Sanity import qualified Prelude #ifdef SMT_PROOF import qualified Proof.Functional.Induction +import qualified Proof.Leakage.Induction #endif import IsaSpec (isaConformanceTests) import ProofSpec (proofTests) @@ -74,7 +75,8 @@ mkSecretPCLeakTest s prog = -- The first three establish that the Pantomime plugin is wired in and actually -- discharging properties -- since pantomime 1821a71 an invalid property no -- longer fails the build, so the negative control has to be asserted here. --- The rest are the refinement proof itself; see "Proof.Functional.Induction". +-- The rest are the proofs themselves; see "Proof.Functional.Induction" and +-- "Proof.Leakage.Induction". sanityTests :: TestTree sanityTests = testGroup @@ -91,15 +93,23 @@ sanityTests = testCase "base case: invariant holds after the reset hop" $ lookup "baseCase" Proof.Functional.Induction.results @?= Just Nothing, testCase "k = 0 inductive step is valid" $ - lookup "indStep0" Proof.Functional.Induction.results @?= Just Nothing, + lookup "indStep" Proof.Functional.Induction.results @?= Just Nothing, testCase "k = 1 inductive step is valid" $ lookup "indStep1" Proof.Functional.Induction.results @?= Just Nothing, testCase "k = 2 inductive step is valid" $ lookup "indStep2" Proof.Functional.Induction.results @?= Just Nothing, testCase "k = 3 inductive step is valid" $ - lookup "indStep3" Proof.Functional.Induction.results @?= Just Nothing - -- The four leakage steps are omitted while Proof.Leakage.Induction is out - -- of the build; see the note in package.yaml. + lookup "indStep3" Proof.Functional.Induction.results @?= Just Nothing, + testCase "leakage base case: simulator matches the first hop" $ + lookup "baseCaseLeak" Proof.Leakage.Induction.results @?= Just Nothing, + testCase "k = 0 leakage step is valid" $ + lookup "indStepLeak" Proof.Leakage.Induction.results @?= Just Nothing, + testCase "k = 1 leakage step is valid" $ + lookup "indStepLeak1" Proof.Leakage.Induction.results @?= Just Nothing, + testCase "k = 2 leakage step is valid" $ + lookup "indStepLeak2" Proof.Leakage.Induction.results @?= Just Nothing, + testCase "k = 3 leakage step is valid" $ + lookup "indStepLeak3" Proof.Leakage.Induction.results @?= Just Nothing ] where verdict :: String -> Maybe String @@ -395,16 +405,17 @@ instance {-# OVERLAPPING #-} (Access f, Arbitrary (f Word)) => Arbitrary (Core.S <*> arbitrary <*> arbitrary <*> arbitrary + <*> arbitrary +-- | Half the time a valid instruction encoding, half the time an arbitrary data +-- word. Whether the core treats it as an instruction is up to the state's +-- 'Core.stateDeExpInstr'. instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Input f) where arbitrary = do - isInstr <- arbitrary mem <- - if isInstr - then fromJust <$> ((encode' <$> arbitrary) `suchThat` isJust) - else arbitrary + oneof + [ fromJust <$> ((encode' <$> arbitrary) `suchThat` isJust), + arbitrary + ] isSecretMem <- arbitrary - pure $ - Input - isInstr - (conditionalSecret isSecretMem mem) + pure $ Input (conditionalSecret isSecretMem mem) From bdddac83fb88496ec668d723b9cc99b4c684d885 Mon Sep 17 00:00:00 2001 From: Kristina Date: Sat, 10 Oct 2026 15:23:22 +0200 Subject: [PATCH 5/8] Add Core.initAt for starting the pipeline at a given PC and register file Six places built an empty pipeline at a chosen PC with a chosen register file by record-updating Core.init: the functional and leakage base cases, the ELF start in Main and BenchmarkSpec (entry point, stack pointer in x2), and the restart after a syscall in ElfLoader and Main (resume PC, result in a0). Give that a name, initAt pc rf, and define the default initial state as init = initAt initPc initRFg. The base cases no longer need the Core.StateG r Identity annotation, nor the forall that brought r into scope for it: the register-file argument fixes the type. Full build with the smt-proof flag passes all symbolic properties; 153 tests pass. Co-Authored-By: Claude Opus 5.5 --- app/Main.hs | 12 +++++------- proof/Proof/Functional/Obligation.hs | 5 ++--- proof/Proof/Leakage/Obligation.hs | 5 ++--- src/Core.hs | 12 ++++++++---- src/Elf/ElfLoader.hs | 3 +-- test/BenchmarkSpec.hs | 7 +++---- 6 files changed, 21 insertions(+), 23 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 4b46a32..cc9033a 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -224,7 +224,7 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta runIOMemT mem $ loadProgram elf let initialSims = P.map (\_ -> simulator @Identity @(IOMemT IO)) [1..optNumInstances] - let initialStates = P.map (\(sim, mem) -> sim { circuitState = (Core.init @Identity @RegFile) { Core.stateFePc = fromIntegral entryOffset, Core.stateRegFile = modifyRF 2 (pure $ ioMemInitSP mem) initRF } }) (P.zip initialSims memInstances) + let initialStates = P.map (\(sim, mem) -> sim { circuitState = Core.initAt (fromIntegral entryOffset) (modifyRF 2 (pure $ ioMemInitSP mem) (initRF @Identity)) }) (P.zip initialSims memInstances) go 0 (P.zip memInstances initialStates) where @@ -253,8 +253,7 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta case mRet of Nothing -> pure (Nothing, True) -- exit Just ret -> do - let s'' = (Core.init :: Core.State Identity) {Core.stateFePc = resumePc, - Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')} + let s'' = Core.initAt resumePc (modifyRF 10 ret (Core.stateRegFile s')) _ <- next s'' o pure (Just Core.initInput, False) _ -> pure (Nothing, False) -- EBreak, SecurityViolation: stop @@ -328,10 +327,9 @@ runExecutable opts@Options{..} = do (secureInstrument optVerbose leakOutputHandle leakDigest finalStateRef) (simulator @PubSec @(SecureIOMemT IO)) { circuitState = - (Core.init @PubSec @RegFile) - { Core.stateFePc = fromIntegral entryOffset, - Core.stateRegFile = modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) initRF - } + Core.initAt + (fromIntegral entryOffset) + (modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) (initRF @PubSec)) } finalState <- readIORef finalStateRef case finalState of diff --git a/proof/Proof/Functional/Obligation.hs b/proof/Proof/Functional/Obligation.hs index 9fcb0e5..86cc88e 100644 --- a/proof/Proof/Functional/Obligation.hs +++ b/proof/Proof/Functional/Obligation.hs @@ -91,13 +91,12 @@ isaAt ipc (Sys st inp mem) = -- gap -- it runs on the real 'Vec'-backed state, where both files are built -- independently. baseCaseObligation :: - forall r m. (RegFileOps r, MemOps m) => r Identity -> m -> RegIdx -> Address -> Address -> Bool + (RegFileOps r, MemOps m) => r Identity -> m -> RegIdx -> Address -> Address -> Bool baseCaseObligation rf mem wr wa pc = driver sys == 1 && invAtFree wr wa isa sys2 where isa = IsaState {isaPc = pc, isaRegFile = rf, isaMem = mem} - st = (Core.init :: Core.StateG r Identity) {Core.stateFePc = pc, Core.stateRegFile = rf} - sys = Sys st Core.initInput mem + sys = Sys (Core.initAt pc rf) Core.initInput mem sys1 = stepSys sys sys2 = stepSys sys1 diff --git a/proof/Proof/Leakage/Obligation.hs b/proof/Proof/Leakage/Obligation.hs index e50b451..b1c73e1 100644 --- a/proof/Proof/Leakage/Obligation.hs +++ b/proof/Proof/Leakage/Obligation.hs @@ -45,15 +45,14 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- afterwards. The register file and memory are arbitrary, as in -- 'Proof.Functional.Obligation.baseCaseObligation'. baseCaseLeakObligation :: - forall r m. (RegFileOps r, MemOps m) => r Identity -> m -> Address -> Bool + (RegFileOps r, MemOps m) => r Identity -> m -> Address -> Bool baseCaseLeakObligation rf mem pc = simDriver Nothing sim == 1 && obs1 == obsOf out1 && obs2 == obsOf out2 && simInv sim2 sys2 where - st = (Core.init :: Core.StateG r Identity) {Core.stateFePc = pc, Core.stateRegFile = rf} - sys = Sys st Core.initInput mem + sys = Sys (Core.initAt pc rf) Core.initInput mem sim = simInit {simStateFePc = pc} (sys1, out1) = stepSysOut sys diff --git a/src/Core.hs b/src/Core.hs index b8e9462..d49d4f3 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -8,6 +8,7 @@ module Core ( initInput, + initAt, init, initCtrl, circuit, @@ -222,10 +223,10 @@ pipe = do initInput :: (Access f) => Input f initInput = Input (pure 0) -init :: forall f r. (Access f, RegFileOps r) => StateG r f -init = +initAt :: (Access f) => Address -> r f -> StateG r f +initAt pc rf = State - { stateFePc = initPc, + { stateFePc = pc, stateDePc = 0, stateDeExpInstr = False, stateExPc = 0, @@ -235,12 +236,15 @@ init = stateMeAddr = 0, stateWbInstr = Nop FirstCycle, stateWbRes = pure 0, - stateRegFile = initRFg, + stateRegFile = rf, stateCtrl = initCtrl, stateHalt = Nothing, stateHaltNextPc = 0 } +init :: forall f r. (Access f, RegFileOps r) => StateG r f +init = initAt initPc initRFg + -- | Initial control lines. initCtrl :: Control f initCtrl = diff --git a/src/Elf/ElfLoader.hs b/src/Elf/ElfLoader.hs index 9c2d5fd..d01cb38 100644 --- a/src/Elf/ElfLoader.hs +++ b/src/Elf/ElfLoader.hs @@ -112,8 +112,7 @@ runElf instr c = go c case mRet of Nothing -> pure () Just ret -> do - let s'' = (Core.init :: Core.State f) {Core.stateFePc = resumePc, - Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')} + let s'' = Core.initAt resumePc (modifyRF 10 ret (Core.stateRegFile s')) go $ sim {circuitInput = Core.initInput, circuitState = s''} Just (Core.EBreak _) -> pure () Just Core.SecurityViolation -> pure () \ No newline at end of file diff --git a/test/BenchmarkSpec.hs b/test/BenchmarkSpec.hs index df15b85..1f06a2b 100644 --- a/test/BenchmarkSpec.hs +++ b/test/BenchmarkSpec.hs @@ -81,10 +81,9 @@ mkBenchmarkTest testName _benchmark = (benchmarkInstrument _benchmark) (sim { circuitState = - (Core.init @Identity @RegFile) - { Core.stateFePc = fromIntegral entryOffset, - Core.stateRegFile = modifyRF 2 (pure $ fromIntegral (base + 0x1000000 - 0x1000)) initRF - } + Core.initAt + (fromIntegral entryOffset) + (modifyRF 2 (pure $ fromIntegral (base + 0x1000000 - 0x1000)) (initRF @Identity)) }) pure () From 000c9ded4b2a9e6a9b2adf51d62a06f1dfc4c9ce Mon Sep 17 00:00:00 2001 From: Kristina Date: Mon, 12 Oct 2026 15:45:38 +0200 Subject: [PATCH 6/8] Remove the low-level leakage models The PC-level leakage models under src/Leak, and Interp, the second encoding of instruction semantics they alone used, are superseded by the ISA-level leakage proof in proof/Proof/Leakage. Remove them, together with TheoremSpec, the generic simulator/non-interference harness that only the (already commented-out) Leak tests used. Main was built around Leak.PC: it ran several instances side by side and compared their per-step Leak.PC leakage. Reduce it to a plain ELF runner: a single instance through ElfLoader.runElf, which already services syscalls, with --verbose and the PubSec --secure-memory mode kept. Gone are --num-instances with the divergence check, and --leakage-output with the BLAKE2 leakage digest (whose handle and digest were never actually written to). The executable no longer depends on binary and blake2. Full build with the smt-proof flag passes all symbolic properties; 153 tests pass. Co-Authored-By: Claude Opus 5.5 --- app/Main.hs | 305 +++--------------- package.yaml | 15 - src/Interp.hs | 56 ---- src/Leak/Arch/Arch.hs | 415 ------------------------ src/Leak/Existence.hs | 35 -- src/Leak/MonitorPC/MonitorLeak.hs | 89 ------ src/Leak/MonitorPC/PC.hs | 75 ----- src/Leak/MonitorPC/Sim.hs | 21 -- src/Leak/PC/ISA.hs | 66 ---- src/Leak/PC/Leak.hs | 475 ---------------------------- src/Leak/PC/PC.hs | 188 ----------- src/Leak/PC/Sim.hs | 240 -------------- src/Leak/PCWithState/PCWithState.hs | 391 ----------------------- src/Leak/SecretPC/Leak.hs | 36 --- src/Leak/SecretPC/PC.hs | 148 --------- test/Spec.hs | 60 ---- test/TheoremSpec.hs | 201 ------------ 17 files changed, 46 insertions(+), 2770 deletions(-) delete mode 100644 src/Interp.hs delete mode 100644 src/Leak/Arch/Arch.hs delete mode 100644 src/Leak/Existence.hs delete mode 100644 src/Leak/MonitorPC/MonitorLeak.hs delete mode 100644 src/Leak/MonitorPC/PC.hs delete mode 100644 src/Leak/MonitorPC/Sim.hs delete mode 100644 src/Leak/PC/ISA.hs delete mode 100644 src/Leak/PC/Leak.hs delete mode 100644 src/Leak/PC/PC.hs delete mode 100644 src/Leak/PC/Sim.hs delete mode 100644 src/Leak/PCWithState/PCWithState.hs delete mode 100644 src/Leak/SecretPC/Leak.hs delete mode 100644 src/Leak/SecretPC/PC.hs delete mode 100644 test/TheoremSpec.hs diff --git a/app/Main.hs b/app/Main.hs index cc9033a..9461fe3 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,114 +2,31 @@ module Main (main) where import Access import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, log, resize) -import Control.Exception (catch, throwIO, Exception) -import Control.Monad (when, forM_) +import Control.Exception (catch) +import Control.Monad (when) import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Core as Core import Data.Functor.Identity +import Data.IORef import Elf.ElfLoader -import Data.Elf (Elf) -import Elf.Syscall (handleSyscall, ProgramExitException(..)) -import Memory.IO (SecureIOMemT, newSecureIOMem, loadSecureProgram, runSecureIOMemT, IOMemT, runIOMemT, newIOMem, loadProgram, IOMem, ioMemInitSP, secureIOMemInitSP) +import Elf.Syscall (ProgramExitException (..), handleSyscall) +import Memory.IO (IOMemT, SecureIOMemT, ioMemInitSP, loadProgram, loadSecureProgram, newIOMem, newSecureIOMem, runIOMemT, runSecureIOMemT, secureIOMemInitSP) import Memory.Types -import RegFile -import Data.Word (Word32) import Numeric (showHex) -import Simulate import Options.Applicative -import System.Exit (exitWith, ExitCode(..)) +import RegFile +import Simulate +import System.Exit (ExitCode (..), exitWith) import Types (Word) import Util -import System.IO -import Data.Maybe (fromMaybe, isJust, isNothing) import qualified Prelude as P import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, undefined, (&&), (++), (||), replicate, zip, take) -import Data.Traversable -import qualified Leak.PC.PC as Leak.PC -import qualified Leak.PC.Leak as Leak -import qualified Leak.SecretPC.PC as SecretLeak.PC -import Data.Binary (encode, Binary (..), Get) -import Data.IORef -import Crypto.Hash.BLAKE2.BLAKE2b (initialize', BLAKE2bState, update, finalize) -import qualified Data.ByteString as BS -import Data.Binary.Builder -import qualified Data.ByteString.Builder as BS - -instance (KnownNat n) => Binary (Unsigned n) where - put = put . toInteger - get = fromInteger <$> (get :: Get Integer) - -instance Binary Leak.BaseInstr - -instance Binary Leak.Instr - -instance Binary Leak.Out - -data LeakageDivergenceException = LeakageDivergenceException - { ldStepCount :: Int - , ldLeakages :: [Leak.Out] - , ldStates :: [Core.State Identity] - , ldInputs :: [Core.Input Identity] - } - -instance Show LeakageDivergenceException where - show (LeakageDivergenceException stepCount leakages states inputs) = - unlines $ - [ "Leakage divergence detected:", - "============================", - "", - "Step count: " P.++ show stepCount, - "", - "Number of instances: " P.++ show (P.length leakages), - "" - ] P.++ - P.concatMap formatInstance (P.zip [0..] (P.zip3 leakages states inputs)) P.++ - [ "", - "Differing leakages:", - "-------------------" - ] P.++ - P.map (\(i, leak) -> "Instance " P.++ show i P.++ ": " P.++ show leak) (P.zip [0..] leakages) - where - formatInstance (idx, (leakage, state, input)) = - [ "Instance " P.++ show idx P.++ ":", - "-------------------------------", - "", - "Input:", - " inputMem: " P.++ show (Core.inputMem input), - "", - "State:", - " PC (fetch): 0x" P.++ showHex (Core.stateFePc state) "", - " PC (decode): 0x" P.++ showHex (Core.stateDePc state) "", - " Expects instruction (decode): " P.++ show (Core.stateDeExpInstr state), - " PC (execute): 0x" P.++ showHex (Core.stateExPc state) "", - " Instruction (execute): " P.++ show (Core.stateExInstr state), - " Instruction (memory): " P.++ show (Core.stateMeInstr state), - " Instruction (writeback): " P.++ show (Core.stateWbInstr state), - " Halt state: " P.++ show (Core.stateHalt state), - "", - "Leakage:", - " " P.++ show leakage, - "" - ] - -instance Exception LeakageDivergenceException - -data StepResult f = StepResult - { stepMem :: IOMem - , stepSim :: CircuitSim (IOMemT IO) (Core.Input Identity) (Core.State Identity) (Core.Output Identity) - , stepNextInput :: Maybe (Core.Input Identity) - , stepContinue :: Bool - , stepFinalState :: Core.State Identity - , stepLeakage :: Leak.Out - } -- | Command line options data Options = Options { optVerbose :: Bool - , optLeakageOutput :: Maybe FilePath , optSecureMemory :: Bool , optExecutable :: String - , optNumInstances :: Int } deriving (Show) -- | Parser for verbose flag @@ -119,14 +36,6 @@ verboseParser = switch <> short 'v' <> help "Enable verbose output (shows PC and instruction trace)" ) --- | Parser for leakage output file argument -leakageOutputParser :: Parser (Maybe FilePath) -leakageOutputParser = optional $ strOption - ( long "leakage-output" - <> short 'l' - <> metavar "FILE" - <> help "Output file for leakage traces" ) - -- | Parser for secure memory flag secureMemoryParser :: Parser Bool secureMemoryParser = switch @@ -140,23 +49,12 @@ executableParser = strArgument ( metavar "EXECUTABLE" <> help "RISC-V ELF executable to run" ) --- | Parser for number of instances -optNumInstancesParser :: Parser Int -optNumInstancesParser = option auto - ( long "num-instances" - <> short 'n' - <> metavar "N" - <> value 1 - <> help "Number of instances to run concurrently (default: 1)" ) - -- | Complete options parser optionsParser :: Parser Options optionsParser = Options <$> verboseParser - <*> leakageOutputParser <*> secureMemoryParser <*> executableParser - <*> optNumInstancesParser -- | Program info for help generation programInfo :: ParserInfo Options @@ -167,17 +65,14 @@ programInfo = info (optionsParser <**> helper) <> footer "Examples:\n\ \ uc-risc-v benchmark/bench_chacha20\n\ \ uc-risc-v --verbose benchmark/bench_blake2b\n\ - \ uc-risc-v --secure-memory benchmark/bench_secure_memory\n\ - \ uc-risc-v --test-suite test/rv32ui/rv32ui-p-add" ) - -generalizedInstrument :: - (Access f, Show (f Word), Show leakOut, MonadIO m, MonadMemory m) => - ((Core.State f) -> (leakState, simState)) -> -- proj function - (leakState -> Core.Input f -> (leakState, leakOut)) -> -- leak function - (leakOut -> BS.ByteString) -> -- serialization function - String -> -- mode name for logging - Bool -> Maybe Handle -> IORef BLAKE2bState -> IORef (Maybe (Core.State f)) -> Instrument f m -generalizedInstrument projFn leakFn serializeFn modeName shouldLog leakageOutput leakDigest finalStateRef s = do + \ uc-risc-v --secure-memory benchmark/bench_secure_memory" ) + +-- | Called by 'runElf' whenever the core halts on a syscall: optionally log the +-- state, remember it as the final state, and service the syscall. +instrument :: + (Access f, Show (f Word), MonadIO m, MonadMemory m) => + String -> Bool -> IORef (Maybe (Core.State f)) -> Instrument f m +instrument modeName shouldLog finalStateRef s = do let pc = Core.stateExPc s when shouldLog $ do @@ -190,116 +85,12 @@ generalizedInstrument projFn leakFn serializeFn modeName shouldLog leakageOutput let s0 = lookupRF 8 rf liftIO $ putStrLn $ "PC=0x" P.++ showHex pc "" P.++ " Instr=0x" P.++ show (Core.stateExInstr s) P.++ " a0=" P.++ show a0 P.++ " s0=" P.++ show s0 P.++ " syscall=" P.++ show a7 - -- Store the current state as the final state liftIO $ writeIORef finalStateRef (Just s) handleSyscall s -generalInstrument :: (Leak.Out -> BS.ByteString) -> Bool -> Maybe Handle -> IORef BLAKE2bState -> IORef (Maybe (Core.State Identity)) -> Instrument Identity (IOMemT IO) -generalInstrument f = generalizedInstrument - Leak.PC.proj - Leak.PC.leak - f - "STANDARD" - -secureInstrument :: (MonadIO m, MonadMemory m) => Bool -> Maybe Handle -> IORef BLAKE2bState -> IORef (Maybe (Core.State PubSec)) -> Instrument PubSec m -secureInstrument = generalizedInstrument - SecretLeak.PC.proj - SecretLeak.PC.leak - (BS.toStrict . encode . show) - "SECURE" - -runNormalMemory :: - Options -> -- Command line options - Elf -> -- ELF file - Word32 -> -- Entry offset - Maybe Handle -> -- Leakage output handle - IORef BLAKE2bState -> -- Leakage digest - IORef (Maybe (Core.State Identity)) -> -- Final state ref (simplified to Identity for now) - IO () -runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalStateRef = do - memInstances <- forM [1..optNumInstances] $ \_ -> newIOMem elf - - forM_ memInstances $ \mem -> do - runIOMemT mem $ loadProgram elf - - let initialSims = P.map (\_ -> simulator @Identity @(IOMemT IO)) [1..optNumInstances] - let initialStates = P.map (\(sim, mem) -> sim { circuitState = Core.initAt (fromIntegral entryOffset) (modifyRF 2 (pure $ ioMemInitSP mem) (initRF @Identity)) }) (P.zip initialSims memInstances) - - go 0 (P.zip memInstances initialStates) - where - go stepCount instances = do - when optVerbose $ putStrLn $ "=== Step " P.++ show stepCount P.++ " ===" - - -- Execute one step for each instance in its own memory context - results <- forM (P.zip instances [(0::Int)..]) $ \((mem, sim@(CircuitSim i s step next)), idx) -> do - (halted, s', mi', leakOutput, sysExit) <- runIOMemT mem $ do - let (leakState, _) = Leak.PC.proj s - let (_, leakOutput) = Leak.PC.leak leakState i - - (s', o) <- step i s - let halted = Core.stateHalt s' - (mi', sysExit) <- case halted of - Nothing -> do - mi'' <- next s' o - pure (mi'', False) - Just (Core.Syscall resumePc) -> do - -- Handle syscall, write return value to a0, resume - let serialize = if idx == 0 - then BS.toStrict . encode - else const BS.empty - let instr = generalInstrument serialize optVerbose leakOutputHandle leakDigest finalStateRef - mRet <- instr s' - case mRet of - Nothing -> pure (Nothing, True) -- exit - Just ret -> do - let s'' = Core.initAt resumePc (modifyRF 10 ret (Core.stateRegFile s')) - _ <- next s'' o - pure (Just Core.initInput, False) - _ -> pure (Nothing, False) -- EBreak, SecurityViolation: stop - pure (halted, s', mi', leakOutput, sysExit) - - when optVerbose $ do - putStrLn $ "Instance " P.++ show idx P.++ ":" - putStrLn $ " PC: 0x" P.++ showHex (Core.stateExPc s') "" - - let newSim = sim { circuitInput = fromMaybe i mi', circuitState = s' } - pure StepResult - { stepMem = mem - , stepSim = newSim - , stepNextInput = mi' - , stepContinue = not sysExit && (isNothing halted || (\case { Just (Core.Syscall _) -> True; _ -> False }) halted) - , stepFinalState = s' - , stepLeakage = leakOutput - } - - -- Extract leakages and check consistency immediately - let leakages = P.map stepLeakage results - case leakages of - [] -> pure () - (firstLeakage:restLeakages) -> case filter (/= firstLeakage) restLeakages of - [] -> when optVerbose $ putStrLn $ "All instances have consistent leakage: " P.++ show firstLeakage - (diff:_) -> do - -- Collect current inputs and states for detailed error reporting - let currentInputs = P.map (circuitInput . stepSim) results - let currentStates = P.map stepFinalState results - throwIO $ LeakageDivergenceException stepCount leakages currentStates currentInputs - - let continuations = P.map stepContinue results - let nextInputs = P.map stepNextInput results - let nextInstances = P.map (\r -> (stepMem r, stepSim r)) results - - let shouldContinue = P.all id continuations && P.all isJust nextInputs - if shouldContinue - then go (stepCount + 1) nextInstances - else do - putStrLn $ "Execution completed after " P.++ show stepCount P.++ " steps" - case results of - (r:_) -> writeIORef finalStateRef (Just (stepFinalState r)) - [] -> pure () - runExecutable :: Options -> IO () -runExecutable opts@Options{..} = do +runExecutable Options{..} = do when optVerbose $ putStrLn $ "Loading ELF file: " P.++ optExecutable elf <- readElf optExecutable @@ -307,49 +98,45 @@ runExecutable opts@Options{..} = do when optVerbose $ do putStrLn $ "Entry point: 0x" P.++ showHex entryOffset "" - putStrLn $ "Number of instances: " P.++ show optNumInstances if optSecureMemory then putStrLn "Starting execution in SECURE MEMORY mode..." else putStrLn "Starting execution in standard mode..." - - leakOutputHandle <- forM optLeakageOutput (flip openFile WriteMode) - leakDigest <- newIORef (initialize' 20 "leakage checksum") if optSecureMemory then do - if optNumInstances == 1 - then do - secureIOMem <- newSecureIOMem elf - finalStateRef <- newIORef Nothing - _ <- runSecureIOMemT secureIOMem $ do - loadSecureProgram elf - runElf - (secureInstrument optVerbose leakOutputHandle leakDigest finalStateRef) - (simulator @PubSec @(SecureIOMemT IO)) - { circuitState = - Core.initAt - (fromIntegral entryOffset) - (modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) (initRF @PubSec)) - } - finalState <- readIORef finalStateRef - case finalState of - Just state | Core.stateHalt state == Just Core.SecurityViolation -> do - putStrLn "Program aborted due to security violation" - _ -> pure () - else do - putStrLn "Secure memory mode with multiple instances not yet implemented" + secureIOMem <- newSecureIOMem elf + finalStateRef <- newIORef Nothing + runSecureIOMemT secureIOMem $ do + loadSecureProgram elf + runElf + (instrument "SECURE" optVerbose finalStateRef) + (simulator @PubSec @(SecureIOMemT IO)) + { circuitState = + Core.initAt + (fromIntegral entryOffset) + (modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) (initRF @PubSec)) + } + finalState <- readIORef finalStateRef + case finalState of + Just state | Core.stateHalt state == Just Core.SecurityViolation -> + putStrLn "Program aborted due to security violation" + _ -> pure () else do - newIORef Nothing >>= runNormalMemory opts elf entryOffset leakOutputHandle leakDigest - - forM_ leakOutputHandle hClose + mem <- newIOMem elf + finalStateRef <- newIORef Nothing + runIOMemT mem $ do + loadProgram elf + runElf + (instrument "STANDARD" optVerbose finalStateRef) + (simulator @Identity @(IOMemT IO)) + { circuitState = + Core.initAt + (fromIntegral entryOffset) + (modifyRF 2 (pure $ ioMemInitSP mem) (initRF @Identity)) + } when optVerbose $ putStrLn "Execution completed successfully" - digest <- finalize 20 <$> readIORef leakDigest - putStr "Leakage digest: " - BS.putStr $ BS.toStrict $ BS.toLazyByteString $ BS.byteStringHex digest - putStrLn "" - main :: IO () main = do opts <- execParser programInfo diff --git a/package.yaml b/package.yaml index cbf1871..987ec75 100644 --- a/package.yaml +++ b/package.yaml @@ -133,24 +133,11 @@ library: - Elf.Syscall - HardwareSim - Instruction - - Interp - ISA - Memory.Types - Memory.Vec - Memory.ST - Memory.IO - - Leak.Arch.Arch - - Leak.PC.ISA - - Leak.PC.Leak - - Leak.PC.PC - - Leak.PC.Sim - - Leak.PCWithState.PCWithState - - Leak.SecretPC.Leak - - Leak.SecretPC.PC - - Leak.MonitorPC.MonitorLeak - - Leak.MonitorPC.PC - - Leak.MonitorPC.Sim - - Leak.Existence - Pretty - RegFile - Simulate @@ -168,8 +155,6 @@ executables: dependencies: - aimcore - optparse-applicative - - binary - - blake2 tests: aimcore-test: diff --git a/src/Interp.hs b/src/Interp.hs deleted file mode 100644 index 8c359b2..0000000 --- a/src/Interp.hs +++ /dev/null @@ -1,56 +0,0 @@ -module Interp where - -import Access -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Core -import Data.Functor.Identity -import Instruction -import Types -import Util -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -data Interp f = Interp - { interpRes :: f Word, - interpAddr :: f (Maybe Address), - interpBranched :: Maybe (f Bool) - } - -interp :: (Access f) => Instruction -> f Word -> f Word -> Address -> Interp f -interp instr r1 r2 pc = - case instr of - RType op rd _ _ -> - Interp (alu op r1 r2) (pure Nothing) Nothing - IType iop rd _ imm -> - let op = - case iop of - Arith op' -> op' - _ -> ADD - alu_res = alu op r1 (pure $ signExtend imm) - in case iop of - Arith {} -> Interp alu_res (pure Nothing) Nothing - Load size sign -> - let addr = fmap (unpack :: Word -> Address) alu_res - in Interp (fmap bitCoerce addr) (fmap Just addr) Nothing - Jump -> - Interp (pure $ pack $ pc + 4) (fmap (Just . unpack) alu_res) Nothing - Env _ -> - Interp (pure 0) (pure Nothing) Nothing - SType size imm _ _ -> - let addr = fmap (unpack :: Word -> Address) (alu ADD r1 (pure $ signExtend imm)) - in Interp (fmap bitCoerce addr) (fmap Just addr) Nothing - BType cmp imm _ _ -> - let branched = branch cmp r1 r2 - jumpAddr = (\b -> if b then Just (pc + unpack (signExtend imm)) else Nothing) <$> branched - branched' = case fromPublic branched of - Just b -> Just (pure b) - Nothing -> Nothing - in Interp (pure 0) jumpAddr branched' - UType Zero rd imm -> - Interp (pure $ imm ++# (0 :: BitVector 12)) (pure Nothing) Nothing - UType PC rd imm -> - let imm' = imm ++# (0 :: BitVector 12) - in Interp (pure $ pack pc + imm') (pure Nothing) Nothing - JType rd imm -> - Interp (pure $ pack $ pc + 4) (pure $ Just $ pc + unpack (signExtend imm)) Nothing - Nop _ -> - Interp (pure 0) (pure Nothing) Nothing diff --git a/src/Leak/Arch/Arch.hs b/src/Leak/Arch/Arch.hs deleted file mode 100644 index 578a858..0000000 --- a/src/Leak/Arch/Arch.hs +++ /dev/null @@ -1,415 +0,0 @@ -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE UndecidableInstances #-} - -module Leak.Arch.Arch () where - --- import Clash.Prelude hiding (Ordering (..), Word, def, init, lift) --- import Control.Monad --- import Control.Monad.RWS --- import Control.Monad.State --- import Control.Monad.Trans.Maybe --- import Data.Maybe (fromJust, fromMaybe, isJust) --- import Data.Monoid --- import Data.Set (Set) --- import qualified Data.Set as S --- import Data.Tuple (swap) --- import GHC.TypeNats --- import Instruction hiding (Jump, decode, halt) --- import qualified Instruction --- import Pipe --- import Regfile --- import qualified Simulate --- import Types --- import Prelude hiding (Ordering (..), Word, const, init, map, not, undefined, (!!), (&&), (||)) --- import qualified Prelude - ----- `fromJust` is safe here because the `fetch` stage unconditionally always reads ----- from memory (and its read may just be superseded by the `memory` stage). --- obs :: Output -> Address --- obs = memAddress . fromJust . getFirst . outMem --- ----- | A computation that may read inputs from (a) register(s). --- data WithReg a --- = Unary RegIdx (Word -> a) --- | Binary RegIdx RegIdx (Word -> Word -> a) --- --- instance Show (WithReg a) where --- show (Unary r _) = --- unwords ["Unary", show r, ""] --- show (Binary r1 r2 _) = --- unwords ["Binary", show r1, show r2, ""] --- --- newtype Comp a = Comp a --- deriving (Show, Eq) --- --- newtype Done a = Done Word --- deriving (Show, Eq) --- --- data JumpType --- = Offset --- | Absolute --- deriving (Show) --- --- data LeakInst f --- = RegStore RegIdx (f (WithReg Word)) --- | MemLoad RegIdx (f (WithReg Word)) --- | MemStore (f (WithReg Word)) --- | Branch (f (WithReg Bool)) Address --- | Jump JumpType Address --- | Nop --- | Halt --- --- deriving instance (Show (f (WithReg Word)), Show (f (WithReg Bool))) => Show (LeakInst f) --- --- getLeakRd :: LeakInst f -> Maybe RegIdx --- getLeakRd (RegStore rd _) = pure rd --- getLeakRd (MemLoad rd _) = pure rd --- getLeakRd _ = Nothing --- --- instrRes :: LeakInst Done -> Maybe Word --- instrRes (RegStore _ (Done w)) = pure w --- instrRes (MemLoad _ (Done w)) = pure w --- instrRes _ = Nothing --- --- class DepReg a where --- deps :: a -> (Maybe RegIdx, Maybe RegIdx) --- --- instance DepReg (WithReg a) where --- deps (Unary r _) = (pure r, Nothing) --- deps (Binary r1 r2 _) = (pure r1, pure r2) --- --- instance (DepReg a) => DepReg (Comp a) where --- deps (Comp a) = deps a --- --- instance DepReg (LeakInst Comp) where --- deps (RegStore _ f) = deps f --- deps (MemLoad _ f) = deps f --- deps (MemStore f) = deps f --- deps _ = (Nothing, Nothing) --- --- data LeakOut = LeakOut --- { leakOutInst :: First (LeakInst Comp), --- leakOutRs1 :: First Word, --- leakOutRs2 :: First Word --- } --- --- instance Semigroup LeakOut where --- LeakOut i r1 r2 <> LeakOut i' r1' r2' = LeakOut (i <> i') (r1 <> r1') (r2 <> r2') --- --- instance Monoid LeakOut where --- mempty = LeakOut mempty mempty mempty --- --- data SimIn = SimIn --- { simInInst :: (LeakInst Comp), --- simInRs1 :: Word, --- simInRs2 :: Word --- } --- --- type LeakM = RWS Input LeakOut () --- --- leak :: LeakM () --- leak = do --- Input _ mem rs1 rs2 <- ask --- case Instruction.decode mem of --- RType op rd r1 r2 -> --- tell $ --- mempty {leakOutInst = pure $ RegStore rd $ Comp $ Binary r1 r2 $ alu op} --- IType iop rd r1 imm -> do --- let op = --- case iop of --- Arith op' -> op' --- _ -> ADD --- comp_res rs1 = alu op rs1 $ signExtend imm --- case iop of --- Arith {} -> --- tell $ --- mempty --- { leakOutInst = pure $ RegStore rd $ Comp $ Unary r1 comp_res --- } --- Load size sign -> do --- let loadExtend rs1 = \case --- (Byte, Signed) -> signExtend $ slice d7 d0 $ comp_res rs1 --- (Byte, Unsigned) -> zeroExtend $ slice d7 d0 $ comp_res rs1 --- (Half, Signed) -> signExtend $ slice d15 d0 $ comp_res rs1 --- (Half, Unsigned) -> signExtend $ slice d15 d0 $ comp_res rs1 --- (Word, _) -> signExtend $ slice d31 d0 $ comp_res rs1 --- comp_val rs1 = loadExtend rs1 (size, sign) --- tell $ --- mempty --- { leakOutInst = --- pure $ --- MemLoad rd $ --- Comp $ --- Unary r1 $ --- bitCoerce . alu ADD (signExtend imm) . comp_val --- } --- SType size imm r1 _ -> --- tell $ --- mempty --- { leakOutInst = pure $ MemStore $ Comp $ Unary r1 $ bitCoerce . alu ADD (signExtend imm) --- } --- BType cmp imm r1 r2 -> --- tell $ --- mempty {leakOutInst = pure $ Branch (Comp $ Binary r1 r2 $ branch cmp) (bitCoerce $ signExtend imm)} --- JType rd imm -> --- tell $ --- mempty {leakOutInst = pure $ Jump Offset (bitCoerce $ signExtend imm)} --- EBREAK -> --- tell $ mempty {leakOutInst = pure Halt} --- _ -> tell $ mempty {leakOutInst = pure Nop} --- ----- UType Zero rd imm -> do ----- let imm' = imm ++# 0 `shiftL` 12 ----- writeRF rd $ imm' ----- pure Nop ----- UType PC rd imm -> do ----- let imm' = imm ++# 0 `shiftL` 12 ----- writeRF rd imm' ----- pure Nop --- --- leakOutToSimIn :: LeakOut -> SimIn --- leakOutToSimIn (LeakOut minst mrs1 mrs2) = --- SimIn --- (fromMaybe Nop $ getFirst minst) --- (fromMaybe 0 $ getFirst mrs1) --- (fromMaybe 0 $ getFirst mrs2) --- --- leakRun :: () -> Input -> ((), SimIn) --- leakRun _s i = fmap leakOutToSimIn $ execRWS leak i _s --- --- type SimM = RWS SimIn (First Address) SimState --- --- stall :: [Stage] -> SimM () --- stall stages = --- modify $ \s -> s {simStall = simStall s <> S.fromList stages} --- --- stallingM :: Stage -> SimM Bool --- stallingM stage = --- S.member stage <$> gets simStall --- --- data Stage = Fe | De | Ex | Mem | Wb --- deriving (Show, Eq, Ord) --- --- data SimState = SimState --- { simFePc :: Address, --- simDePc :: Address, --- simExPc :: Address, --- simJumpAddr :: Maybe Address, --- simExInstr :: LeakInst Comp, --- simExRes :: Word, --- simMemInstr :: LeakInst Done, --- simMemRes :: Word, --- simWbInstr :: LeakInst Done, --- simStall :: Set Stage, --- simHalt :: Bool --- } --- deriving (Show) --- --- withReg :: WithReg a -> SimM a --- withReg (Unary _ f) = --- f <$> asks simInRs1 --- withReg (Binary _ _ f) = --- f <$> asks simInRs1 <*> asks simInRs2 --- --- initSim :: SimState --- initSim = --- SimState --- { simFePc = 4 * 50, --- simDePc = 0, --- simExPc = 0, --- simJumpAddr = Nothing, --- simExInstr = Nop, --- simExRes = 0, --- simMemInstr = Nop, --- simMemRes = 0, --- simWbInstr = Nop, --- simStall = mempty, --- simHalt = False --- } --- --- simFetch :: SimM () --- simFetch = do --- s <- get --- stalling <- stallingM Fe --- unless stalling $ do --- modify $ \s -> --- s --- { simFePc = fromMaybe (simFePc s + 4) (simJumpAddr s), --- simDePc = simFePc s --- } --- tell $ pure $ simFePc s --- --- simDecode :: SimM () --- simDecode = do --- s <- get --- instr <- asks simInInst --- instr' <- --- case instr of --- Jump Offset offset -> pure $ Jump Absolute $ simDePc s + offset --- _ -> pure instr --- case instr' of --- MemLoad {} -> stall [Fe] --- _ -> pure () --- ex_ir <- gets simExInstr --- when (loadHazard instr' ex_ir) $ --- stall [De] --- stalling <- stallingM De --- modify $ \s -> --- s --- { simExInstr = --- if stalling --- then Nop --- else instr', --- simExPc = simDePc s --- } --- where --- loadHazard :: LeakInst Comp -> LeakInst Comp -> Bool --- loadHazard de_ir ex_ir@(MemLoad {}) = isJust $ do --- let (mr1, mr2) = deps de_ir --- mrd = getLeakRd ex_ir --- (guard =<< (==) <$> mrd <*> mr1) --- <|> (guard =<< (==) <$> mrd <*> mr2) --- loadHazard _ _ = False --- --- simExecute :: SimM () --- simExecute = do --- instr <- gets simExInstr --- instr' <- case instr of --- RegStore rd f -> --- RegStore rd . Done <$> withRegFwd f --- MemLoad rd f -> do --- MemLoad rd . Done <$> withRegFwd f --- MemStore f -> do --- MemStore . Done <$> withRegFwd f --- Branch f offset -> do --- doBranch <- withRegFwd f --- if doBranch --- then do --- pc <- gets simExPc --- let pc' = pc + offset --- modify $ \s -> s {simJumpAddr = pure pc'} --- stall [De] --- pure $ Jump Absolute pc' --- else pure Nop --- Jump Absolute addr -> do --- stall [De] --- modify $ \s -> s {simJumpAddr = pure addr} --- pure $ Jump Absolute addr --- Nop -> pure Nop --- Halt -> pure Halt --- modify $ \s -> s {simMemInstr = instr'} --- where --- withRegFwd :: (Comp (WithReg a)) -> SimM a --- withRegFwd (Comp (Unary r1 f)) = --- f <$> regFwd r1 (asks simInRs1) --- withRegFwd (Comp (Binary r1 r2 f)) = --- f <$> regFwd r1 (asks simInRs1) <*> regFwd r2 (asks simInRs2) --- --- regFwd :: RegIdx -> SimM Word -> SimM Word --- regFwd r defm = do --- mw <- runMaybeT $ getFwdReg r --- case mw of --- Nothing -> defm --- Just w -> pure w --- --- getFwdReg :: RegIdx -> MaybeT SimM Word --- getFwdReg r = --- do --- s <- get --- me_rd <- MaybeT $ getLeakRd <$> gets simMemInstr --- wb_rd <- MaybeT $ getLeakRd <$> gets simWbInstr --- fwd (hazardRW r me_rd) (simMemInstr s) --- <|> fwd (hazardRW r wb_rd) (simWbInstr s) --- where --- fwd cond instr = --- MaybeT $ pure $ instrRes instr --- --- hazardRW :: RegIdx -> RegIdx -> Bool --- hazardRW r rd = --- rd /= 0 && r == rd --- --- simMemory :: SimM () --- simMemory = do --- instr <- gets simMemInstr --- case instr of --- MemLoad _ (Done addr) -> do --- tell $ pure $ bitCoerce addr --- stall [Fe] --- MemStore (Done addr) -> do --- tell $ pure $ bitCoerce addr --- stall [Fe] --- Jump {} -> --- stall [De] --- _ -> pure () --- --- modify $ \s -> s {simWbInstr = simMemInstr s} --- --- simWriteback :: SimM () --- simWriteback = do --- instr <- gets simWbInstr --- halted <- gets simHalt --- --- when halted $ do --- tell $ pure 0 --- --- case instr of --- Halt -> do --- modify $ \s -> --- s --- { simMemInstr = Nop, --- simExInstr = Nop, --- simHalt = True --- } --- tell $ pure 0 --- RegStore rd val -> pure () --- MemLoad {} -> stall [De] --- MemStore (Done addr) -> --- stall [De] --- _ -> pure () --- --- simTick :: SimM () --- simTick = do --- modify $ \s -> s {simStall = mempty, simJumpAddr = empty} --- simWriteback --- simMemory --- simExecute --- simDecode --- simFetch --- --- simRun :: SimState -> SimIn -> (SimState, Address) --- simRun s i = (fromMaybe 0 . getFirst) <$> execRWS simTick i s --- --- simLeakRun :: ((), SimState) -> Input -> (((), SimState), Address) --- simLeakRun (_ls, ss) input = ((_ls', ss'), addr) --- where --- (_ls', simin) = leakRun _ls input --- (ss', addr) = simRun ss simin --- --- simIO :: forall n. (KnownNat n) => Vec n Byte -> IO () --- simIO = --- void --- . runRWST --- (simulate initInput initPipe () initSim) --- () --- . flip Simulate.Mem initRF --- where --- simulate i s leak_s sim_s = --- void $ forever $ do --- lift $ putStrLn "Press Enter to continue." --- _ <- lift getLine --- (i', s', _o) <- Simulate.report $ Simulate.simStep i s --- let ((leak_s', sim_s'), leak_addr) = simLeakRun (leak_s, sim_s) i --- lift $ --- putStrLn $ --- unlines --- [ "Leak out:", --- "--------------------", --- show leak_addr, --- "Leak state:", --- "--------------------", --- show leak_s, --- "Sim state:", --- "--------------------", --- show sim_s --- ] --- simulate i' s' leak_s' sim_s' diff --git a/src/Leak/Existence.hs b/src/Leak/Existence.hs deleted file mode 100644 index 790134c..0000000 --- a/src/Leak/Existence.hs +++ /dev/null @@ -1,35 +0,0 @@ -module Leak.Existence (Fiber, simulatorFor) where - -import Pantomime -import Pantomime.Clash.NonInterference (SimulatorExistNI (..)) - --- | Fiber is a function such that: --- --- @ --- presim = \(si, i) -> --- let (sl, ss) = projection si --- (sl', x) = leakage sl i --- in (ss, x) --- @ --- --- For all x : (si, i), we have presim(fiber(presim(x))) = presim(x) --- --- In the paper, this is constructed as the Tick function, where --- fiber(y) = first element of {x ∈ (si, i) | presim(x) = y}, --- but in practice you would want to write one that is more efficient. -type Fiber si i ss l = (ss, l) -> (si, i) - --- | Given a non-interference instance that satisfies --- tickStateCorrespondence and projectionCoherence, --- and a fiber function, we can construct a simulator --- as per lemma 3.18 in the paper. -simulatorFor :: - SimulatorExistNI si sl ss i l o -> - Fiber si i ss l -> - (ss, l) -> - (ss, o) -simulatorFor SimulatorExistNI {..} fiber (ss, l) = - let (si, i) = fiber (ss, l) - (si', o) = implementation si i - (_, ss') = projection si' - in (ss', o) \ No newline at end of file diff --git a/src/Leak/MonitorPC/MonitorLeak.hs b/src/Leak/MonitorPC/MonitorLeak.hs deleted file mode 100644 index 1ca0f4d..0000000 --- a/src/Leak/MonitorPC/MonitorLeak.hs +++ /dev/null @@ -1,89 +0,0 @@ -module Leak.MonitorPC.MonitorLeak ( - LeakMonitor (..), - (^&^), - monitorPC, - Instr (..), - BaseInstr (..), - toLeakInstr, - nop', -) -where - -import Control.Monad.Identity -import qualified Core -import Instruction -import Types - --- A leakage is a mealy machine with state sl, input ii, output ol, --- equipped with a state projection from si to sl. -data LeakMonitor si ii sl ol = LeakMonitor - { leakCircuit :: (sl -> ii -> (sl, ol)) - , leakProject :: si -> sl - } - --- Combine two leakages into a leakage that leaks both. -(^&^) :: LeakMonitor si ii sl1 ol1 -> LeakMonitor si ii sl2 ol2 -> LeakMonitor si ii (sl1, sl2) (ol1, ol2) -(LeakMonitor f1 p1) ^&^ (LeakMonitor f2 p2) = LeakMonitor leak (\s -> (p1 s, p2 s)) - where - leak (sl1, sl2) i = ((sl1', sl2'), (o1, o2)) - where - (sl1', o1) = f1 sl1 i - (sl2', o2) = f2 sl2 i - -monitorPC :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity, Core.State Identity) (Instr, Maybe Address) -monitorPC = monitorInstructionType ^&^ monitorJumpAddress - -data BaseInstr - = Jump' - | Load' - | Store' - | Other' - | Call' - | Break' - deriving (Show, Eq) - -data Instr = Instr BaseInstr (Maybe RegIdx) (Maybe RegIdx) - deriving (Show, Eq) - -toLeakInstr :: Instruction -> Instr -toLeakInstr input = Instr (mkInstr input) (getRs1' input) (getRs2' input) - where - getRs1' (Nop _) = Nothing - getRs1' i = getRs1 i - getRs2' (Nop _) = Nothing - getRs2' i = getRs2 i - - mkInstr :: Instruction -> BaseInstr - mkInstr instr = case instr of - RType{} -> Other' - IType iop _ _ _ -> case iop of - Arith{} -> Other' - Load{} -> Load' - Jump -> Jump' - Env Break -> Break' - Env Call -> Call' - SType{} -> Store' - BType{} -> Jump' - UType Zero _ _ -> Other' - UType PC _ _ -> Other' - JType{} -> Jump' - Nop _ -> Other' - -nop' :: Instr -nop' = toLeakInstr nop - -monitorInstructionType :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity) Instr -monitorInstructionType = LeakMonitor leak id - where - leak :: Core.State Identity -> Core.Input Identity -> (Core.State Identity, Instr) - leak s i = (fst (Core.circuit s i), instr) - where - instr - | Core.stateDeExpInstr s = toLeakInstr $ decode' $ runIdentity $ Core.inputMem i - | otherwise = nop' - -monitorJumpAddress :: LeakMonitor (Core.State Identity) (Core.Input Identity) (Core.State Identity) (Maybe Address) -monitorJumpAddress = LeakMonitor leak id - where - leak :: Core.State Identity -> Core.Input Identity -> (Core.State Identity, Maybe Address) - leak s i = let (s', _) = Core.circuit s i in (s', Core.ctrlExJumpAddr $ Core.stateCtrl s') \ No newline at end of file diff --git a/src/Leak/MonitorPC/PC.hs b/src/Leak/MonitorPC/PC.hs deleted file mode 100644 index bc05a26..0000000 --- a/src/Leak/MonitorPC/PC.hs +++ /dev/null @@ -1,75 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - -module Leak.MonitorPC.PC - ( obs, - proj, - leak, - Sim.State, - -- comment them out to disable Pantomime checks for faster compilation - -- tickStateCorrespondence, - -- projectionCoherence, - ) -where - -import Access -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad -import Core (Input (..), MemAccess (..), Output (..)) -import qualified Core -import Data.Functor.Identity -import Data.Maybe (isJust, isNothing) -import qualified Leak.MonitorPC.MonitorLeak as Leak -import qualified Leak.MonitorPC.Sim as Sim -import Types -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -stateless :: (a -> b) -> () -> a -> ((), b) -stateless f _ x = ((), f x) - -obs :: () -> Output Identity -> ((), Maybe Address) -obs = stateless obs' - -obs' :: Output Identity -> Maybe Address -obs' o_sim = do - mem <- outMem o_sim - guard $ memIsInstr mem - pure $ memAddress mem - -leak :: (Core.State Identity, Core.State Identity) -> Input Identity -> ((Core.State Identity, Core.State Identity), (Leak.Instr, Maybe Address)) -leak = Leak.leakCircuit Leak.monitorPC - -proj :: Core.State Identity -> ((Core.State Identity, Core.State Identity), Sim.State) -proj s = (ts, ss) - where - ts = Leak.leakProject Leak.monitorPC s - halted = isJust (Core.stateHalt s) - ss = - Sim.State - { Sim.stateFePc = if halted then 0 else Core.stateFePc s, - Sim.stateDePc = if halted then 0 else Core.stateDePc s, - Sim.stateExPc = if halted then 0 else Core.stateExPc s, - Sim.stateExInstr = if halted then Leak.nop' else Leak.toLeakInstr $ Core.stateExInstr s, - Sim.stateMemInstr = if halted then Leak.nop' else killJump $ Leak.toLeakInstr $ Core.stateMeInstr s, - Sim.stateMemRes = if halted then 0 else unAccess $ Core.stateMeRes s, - Sim.stateWbInstr = if halted then Leak.nop' else killJump $ Leak.toLeakInstr $ Core.stateWbInstr s, - Sim.stateWbRes = if halted then 0 else unAccess $ Core.stateWbRes s, - Sim.stateHalt = halted, - Sim.stateStallFetch = not halted && toStallFetch (Core.stateCtrl s), - Sim.stateStallDecode = not halted && toStallDecode (Core.stateCtrl s), - Sim.stateJumpAddr = if halted then Nothing else Core.ctrlExJumpAddr $ Core.stateCtrl s, - Sim.stateFirstCycle = not halted && isNothing (Core.stateHalt s) - } - - killJump :: Leak.Instr -> Leak.Instr - killJump (Leak.Instr (Leak.Jump' {}) _ _) = Leak.nop' - killJump i = i - - toStallFetch :: Core.Control Identity -> Bool - toStallFetch ctrl = - Core.ctrlMeMemInstr ctrl - || isJust (Core.ctrlExJumpAddr ctrl) - - toStallDecode :: Core.Control Identity -> Bool - toStallDecode ctrl = - isJust (Core.ctrlDeLoadHazard ctrl) - || isJust (Core.ctrlExJumpAddr ctrl) diff --git a/src/Leak/MonitorPC/Sim.hs b/src/Leak/MonitorPC/Sim.hs deleted file mode 100644 index 15db5a6..0000000 --- a/src/Leak/MonitorPC/Sim.hs +++ /dev/null @@ -1,21 +0,0 @@ -module Leak.MonitorPC.Sim where - -import Leak.MonitorPC.MonitorLeak as Leak -import Types - -data State = State - { stateFePc :: Address, - stateDePc :: Address, - stateExPc :: Address, - stateExInstr :: Leak.Instr, - stateMemInstr :: Leak.Instr, - stateMemRes :: Types.Word, - stateWbInstr :: Leak.Instr, - stateWbRes :: Types.Word, - stateJumpAddr :: Maybe Address, - stateStallFetch :: Bool, - stateStallDecode :: Bool, - stateHalt :: Bool, - stateFirstCycle :: Bool - } - deriving (Show, Eq) diff --git a/src/Leak/PC/ISA.hs b/src/Leak/PC/ISA.hs deleted file mode 100644 index ed19741..0000000 --- a/src/Leak/PC/ISA.hs +++ /dev/null @@ -1,66 +0,0 @@ -module Leak.PC.ISA (leak) where - -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad -import Control.Monad.RWS -import Control.Monad.State -import Control.Monad.Trans.Maybe -import Core (Input) -import qualified Core -import Data.Functor.Identity -import Data.Maybe (fromMaybe, isJust) -import Data.Monoid -import qualified Instruction as Core -import Interp -import qualified Leak.PC.Leak as Leak -import qualified Simulate -import Memory.Types -import Memory.Vec () -import Types -import Util -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -leak :: Vec PROG_SIZE Word -> [Leak.Out] -leak = Prelude.map (\(_, o, _) -> o) . runSimulator watch - -simulator :: - forall m. - ( MonadState ((Core.State Identity, Core.Output Identity), Simulate.Mem MEM_SIZE_BYTES) m - ) => - CircuitSim m (Input Identity) Leak.State Leak.Out -simulator = - CircuitSim - { circuitInput = Core.initInput, - circuitState = Leak.init, - circuitStep = step, - circuitNext = next - } - where - step :: Input Identity -> Leak.State -> m (Leak.State, Leak.Out) - step i s = do - ((s_sim, _), mem) <- get - let (res_sim@(_, o_sim), mem') = runState (circuitStep Simulate.simulator i s_sim) mem - put (res_sim, mem') - let (s', leakInstr) = Leak.circuit s i - pure (s', leakInstr) - - next :: Leak.State -> Leak.Out -> m (Maybe (Input Identity)) - next _ _out = do - ((s_sim, o_sim), mem) <- get - let (mi, mem') = runState (circuitNext Simulate.simulator s_sim o_sim) mem - modify $ \(s, _mem) -> (s, mem') - pure mi - -runSimulator :: - ( CircuitSim - (State ((Core.State Identity, Core.Output Identity), Simulate.Mem MEM_SIZE_BYTES)) - (Input Identity) - Leak.State - Leak.Out -> - State ((Core.State Identity, Core.Output Identity), Simulate.Mem MEM_SIZE_BYTES) a - ) -> - Vec PROG_SIZE Word -> - a -runSimulator f prog = evalState (f Leak.PC.ISA.simulator) s - where - s = ((Core.init, mempty), Simulate.Mem (mkRAM prog)) diff --git a/src/Leak/PC/Leak.hs b/src/Leak/PC/Leak.hs deleted file mode 100644 index 1f8684b..0000000 --- a/src/Leak/PC/Leak.hs +++ /dev/null @@ -1,475 +0,0 @@ -module Leak.PC.Leak - ( pipe, - circuit, - init, - nop, - isLoad, - loadHazard, - mkInstr, - mkDeps, - Instr (..), - BaseInstr (..), - State (..), - Out (..), - ) -where - -import Access -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad -import Control.Monad.RWS -import Control.Monad.Trans.Maybe -import Core (Input, HaltState (..)) -import qualified Core -import Data.Functor.Identity -import Data.Maybe (fromMaybe, isJust) -import Data.Monoid -import qualified Instruction as Instr -import Interp -import RegFile -import Memory.Types -import Types -import Util -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -type LeakM = RWS (Input Identity) Out State - -data BaseInstr - = Jump - | Branch - | Load RegIdx - | Store - | Other - | Call - | Break - | Nop Instr.Reason4Stall - deriving (Show, Eq, Generic) - -data Instr = Instr - { instrBase :: BaseInstr, - instrDeps :: (Maybe RegIdx, Maybe RegIdx) - } - deriving (Show, Eq, Generic) - -isLoad :: Instr -> Bool -isLoad (Instr (Load {}) _) = True -isLoad (Instr Call _) = True -- syscalls behaves like load to a0 -isLoad _ = False - -loadHazard :: Instr -> Instr -> Bool -loadHazard (Instr _ (dep1, dep2)) (Instr (Load rd) _) = - fromMaybe False ((rd ==) <$> dep1) - || fromMaybe False ((rd ==) <$> dep2) -loadHazard _ _ = False - -nop :: Instr -nop = Instr (Nop Instr.FirstCycle) (Nothing, Nothing) - -data State = State - { stateFePc :: Address, - stateDePc :: Address, - stateDeExpInstr :: Bool, - stateExPc :: Address, - stateExInstr :: Instr.Instruction, - stateMemInstr :: Instr.Instruction, - stateMemRes :: Word, - stateMemVal :: Word, - stateWbInstr :: Instr.Instruction, - stateWbRes :: Word, - stateRegFile :: RegFile Identity, - stateMeMemInstr :: Bool, - stateHalt :: Maybe HaltState, - stateMeRegFwd :: Maybe (RegIdx, Word), - stateWbRegFwd :: Maybe (RegIdx, Word), - stateJumpAddr :: Maybe Address, - stateDeLoadHazard :: Maybe Address, - stateDeCall :: Bool, - stateFirstCycle :: Bool - } - deriving (Show, Eq) - -init :: State -init = - State - { stateFePc = initPc, - stateDePc = 0, - stateDeExpInstr = False, - stateExPc = 0, - stateExInstr = Instr.Nop Instr.FirstCycle, - stateMemInstr = Instr.Nop Instr.FirstCycle, - stateMemRes = 0, - stateMemVal = 0, - stateWbInstr = Instr.Nop Instr.FirstCycle, - stateWbRes = 0, - stateRegFile = initRF, - stateMeMemInstr = False, - stateHalt = Nothing, - stateMeRegFwd = Nothing, - stateWbRegFwd = Nothing, - stateJumpAddr = Nothing, - stateDeLoadHazard = Nothing, - stateDeCall = False, - stateFirstCycle = True - } - -data Out = Out - { outInstr :: First Instr, - outJumpAddr :: First Address, - outRs1 :: First RegIdx, - outRs2 :: First RegIdx, - outMeMemInstr :: First Bool, - outHalt :: First Bool, - outBranchTaken :: First Bool, - outJumpAddrValid :: First Bool - } - deriving (Show, Eq, Generic) - -instance Semigroup Out where - Out i1 a1 rs11 rs21 m1 h1 b1 v1 <> Out i2 a2 rs12 rs22 m2 h2 b2 v2 = - Out (i1 <> i2) (a1 <> a2) (rs11 <> rs12) (rs21 <> rs22) (m1 <> m2) (h1 <> h2) (b1 <> b2) (v1 <> v2) - -instance Monoid Out where - mempty = Out mempty mempty mempty mempty mempty mempty mempty mempty - -setMeMemInstr :: LeakM () -setMeMemInstr = do - modify $ \s -> s {stateMeMemInstr = True} - tell $ mempty {outMeMemInstr = pure True} - -outputNothing :: LeakM () -outputNothing = tell mempty - -fetch :: LeakM () -fetch = do - pc <- gets stateFePc - mJumpAddr <- gets stateJumpAddr - deLoadHazard <- gets stateDeLoadHazard - deCall <- gets stateDeCall - meMemInstr <- gets stateMeMemInstr - - let stall = deCall || meMemInstr - - let next_pc = - fromMaybe - (fromMaybe - (if stall then pc else pc + 4) - deLoadHazard) - mJumpAddr - - modify $ \s -> - s - { stateFePc = next_pc, - stateDePc = pc, - -- The core fetches unless the memory stage uses the bus; a call does - -- not stop it. - stateDeExpInstr = not meMemInstr - } - -decode :: LeakM () -decode = do - input <- ask - expInstr <- gets stateDeExpInstr - let instr - | expInstr = - Instr.decode' $ runIdentity $ Core.inputMem input - | otherwise = Instr.Nop Instr.MemoryBusBusy - - when (Instr.isCall instr) $ do - modify $ \s -> s {stateDeCall = True} - - exInstr <- gets stateExInstr - mJumpAddr <- gets stateJumpAddr - firstCycle <- gets stateFirstCycle - - let branch_first_cycle = exInstr == Instr.Nop Instr.JumpFirstCycle - let load_hazard_current_cycle = Instr.loadHazard instr exInstr - let load_hazard_first_cycle = exInstr == Instr.Nop Instr.LoadHazardFirstCycle - let call_current_cycle = Instr.isCall exInstr - - let isSecretInstr = case fromPublic (Core.inputMem input) of Nothing -> True; _ -> False - - let ir' = - -- If a branch was taken in this cycle, we stall. - if isJust mJumpAddr then Instr.Nop Instr.JumpFirstCycle - -- If a branch was taken in the previous cycle, we stall. - else if branch_first_cycle then Instr.Nop Instr.JumpSecondCycle - -- If there is a load hazard with the instruction executed in this cycle, we stall. - else if load_hazard_current_cycle then Instr.Nop Instr.LoadHazardFirstCycle - -- If there was a load hazard in the previous cycle, we stall. - else if load_hazard_first_cycle then Instr.Nop Instr.LoadHazardSecondCycle - -- If a syscall is executed in this cycle, we stall. - else if call_current_cycle then Instr.Nop Instr.Halted - -- If this is the first cycle, the instruction to decode is gibberish from memory. - else if firstCycle then Instr.Nop Instr.FirstCycle - -- If memory is busy, we stall. - else if not expInstr then Instr.Nop Instr.MemoryBusBusy - -- If we are in SecurityViolation state, we stall. - else if isSecretInstr then Instr.Nop Instr.Halted - -- Otherwise we process the decoded instruction. - else instr - - when isSecretInstr $ modify $ \s -> s {stateHalt = Just SecurityViolation} - - let rs1Idx = fromMaybe 0 $ Instr.getRs1 ir' - let rs2Idx = fromMaybe 0 $ Instr.getRs2 ir' - - tell $ - mempty - { outInstr = - pure $ - Instr - { instrBase = mkInstr ir', - instrDeps = mkDeps ir' - }, - outRs1 = pure rs1Idx, - outRs2 = pure rs2Idx - } - - when load_hazard_current_cycle $ do - pc <- gets stateDePc - modify $ \s -> s {stateDeLoadHazard = Just pc} - - when (Instr.isCall ir') $ - modify $ \s -> s {stateDeCall = True} - - modify $ \s -> - s - { stateExInstr = ir', - stateExPc = stateDePc s - } - -mkDeps :: Instr.Instruction -> (Maybe RegIdx, Maybe RegIdx) -mkDeps instr = (noZero $ Instr.getRs1 instr, noZero $ Instr.getRs2 instr) - where - noZero (Just 0) = Nothing - noZero r = r - -mkInstr :: Instr.Instruction -> BaseInstr -mkInstr instr - | instr == Instr.nop = Nop Instr.FirstCycle - | otherwise = case instr of - Instr.RType {} -> Other - Instr.IType iop rd _ _ -> - case iop of - Instr.Arith {} -> - Other - Instr.Load {} -> - Load rd - Instr.Jump -> - Jump - Instr.Env Instr.Break -> - Break - Instr.Env Instr.Call -> - Call - Instr.SType {} -> - Store - Instr.BType {} -> - Branch - Instr.UType Instr.Zero _ _ -> - Other - Instr.UType Instr.PC _ _ -> do - Other - Instr.JType {} -> - Jump - Instr.Nop r -> - Nop r - -execute :: LeakM () -execute = do - instr <- gets stateExInstr - - let r1M :: LeakM (Identity Word) - r1M = do - ir <- gets stateExInstr - rf <- gets stateRegFile - Identity <$> (regWithFwd Instr.getRs1 (unAccess $ lookupRF (fromMaybe 0 $ Instr.getRs1 ir) rf)) - - r2M :: LeakM (Identity Word) - r2M = do - ir <- gets stateExInstr - rf <- gets stateRegFile - Identity <$> (regWithFwd Instr.getRs2 (unAccess $ lookupRF (fromMaybe 0 $ Instr.getRs2 ir) rf)) - - regWithFwd :: (Instr.Instruction -> Maybe RegIdx) -> Word -> LeakM Word - regWithFwd getR def = do - ir <- gets stateExInstr - let checkForFwd line = do - (fwdIdx, fwdVal) <- MaybeT $ gets line - guard (hazardRW getR ir fwdIdx) - pure fwdVal - fmap - (fromMaybe def) - $ runMaybeT - $ checkForFwd stateMeRegFwd <|> checkForFwd stateWbRegFwd - - interp_res <- interp instr <$> r1M <*> r2M <*> gets stateExPc - - modify $ \s -> s {stateMemInstr = instr, stateMemVal = 0} - - case instr of - Instr.IType Instr.Jump _ _ _ -> - case fromPublic (interpAddr interp_res) of - Just (Just addr) -> do - informJumpAddr addr - tell $ mempty { outJumpAddrValid = pure True } - _ -> unless (isPublic (interpAddr interp_res)) $ - modify $ \s -> s {stateHalt = Just SecurityViolation} - Instr.BType {} -> - case (fromPublic (interpAddr interp_res), interpBranched interp_res) of - (Just mAddr, Just branched) -> - case fromPublic branched of - Just True -> do - case mAddr of - Just addr -> informJumpAddr addr - Nothing -> modify $ \s -> s {stateHalt = Just SecurityViolation} - tell $ mempty { outBranchTaken = pure True } - Just False -> tell $ mempty { outBranchTaken = pure False } - Nothing -> modify $ \s -> s {stateHalt = Just SecurityViolation} - _ -> unless (isPublic (interpAddr interp_res)) $ - modify $ \s -> s {stateHalt = Just SecurityViolation} - Instr.JType _ _ -> - case fromPublic (interpAddr interp_res) of - Just (Just addr) -> do - informJumpAddr addr - tell $ mempty { outJumpAddrValid = pure True } - _ -> unless (isPublic (interpAddr interp_res)) $ - modify $ \s -> s {stateHalt = Just SecurityViolation} - Instr.SType {} -> do - r2Val <- unAccess <$> r2M - modify $ \s -> s { stateMemVal = r2Val } - _ -> pure () - - modify $ \s -> s {stateMemRes = runIdentity $ interpRes interp_res} - where - informJumpAddr :: Address -> LeakM () - informJumpAddr jump_addr = do - tell $ mempty {outJumpAddr = pure jump_addr} - modify $ \s -> s {stateJumpAddr = pure jump_addr} - - hazardRW :: (Instr.Instruction -> Maybe RegIdx) -> Instr.Instruction -> RegIdx -> Bool - hazardRW getR src rd = isJust $ do - rs <- getR src - guard $ rd /= 0 && rs == rd - -memory :: LeakM () -memory = do - instr <- gets stateMemInstr - res <- gets stateMemRes - - let shouldForward = case instr of - Instr.RType {} -> True - Instr.IType (Instr.Arith _) _ _ _ -> True - Instr.JType {} -> True - Instr.IType Instr.Jump _ _ _ -> True - Instr.UType {} -> True - _ -> False - - when shouldForward $ try $ do - rd <- MaybeT $ pure $ Instr.getRd instr - lift $ modify $ \s -> s {stateMeRegFwd = pure (rd, res)} - - let isSecretAddr = case fromPublic (Identity res) of Nothing -> True; _ -> False - - case instr of - Instr.IType Instr.Load {} _ _ _ -> do - modify $ \s -> s {stateMeRegFwd = Nothing} - if isSecretAddr - then do - modify $ \s -> s {stateHalt = Just SecurityViolation} - tell $ mempty {outMeMemInstr = pure False} - else setMeMemInstr - Instr.IType (Instr.Env Instr.Call) _ _ _ -> do - modify $ \s -> s {stateMeRegFwd = Nothing} - setMeMemInstr - Instr.SType {} -> do - if isSecretAddr - then do - modify $ \s -> s {stateHalt = Just SecurityViolation} - tell $ mempty {outMeMemInstr = pure False} - else setMeMemInstr - _ -> pure () - - modify $ \s -> - s - { stateWbInstr = instr, - stateWbRes = res - } - -writeback :: LeakM () -writeback = do - input <- asks Core.inputMem - instr <- gets stateWbInstr - stateHalted <- gets stateHalt - res <- gets stateWbRes - - when (isJust stateHalted) $ do - outputNothing - tell $ mempty { outHalt = pure True } - - when (Instr.isBreak instr) $ do - modify $ \s -> - s - { stateMemInstr = Instr.nop, - stateExInstr = Instr.nop, - stateHalt = Just (EBreak 0) - } - outputNothing - - let shouldForward = case instr of - Instr.RType {} -> True - Instr.IType (Instr.Arith _) _ _ _ -> True - Instr.IType (Instr.Load {}) _ _ _ -> True - Instr.JType {} -> True - Instr.IType Instr.Jump _ _ _ -> True - Instr.UType {} -> True - _ -> False - - when shouldForward $ try $ do - rd <- MaybeT $ pure $ Instr.getRd instr - lift $ modify $ \s -> s {stateWbRegFwd = pure (rd, res)} - - case instr of - Instr.RType _ rd _ _ -> - modify $ \s -> s {stateRegFile = modifyRF rd (pure res) (stateRegFile s)} - Instr.IType (Instr.Arith _) rd _ _ -> - modify $ \s -> s {stateRegFile = modifyRF rd (pure res) (stateRegFile s)} - Instr.IType (Instr.Load size sign) rd _ _ -> do - let val = Instr.loadExtend size sign (unAccess input) - modify $ \s -> s {stateRegFile = modifyRF rd (pure val) (stateRegFile s)} - modify $ \s -> s {stateWbRegFwd = pure (rd, val)} - Instr.JType rd _ -> - modify $ \s -> s {stateRegFile = modifyRF rd (pure res) (stateRegFile s)} - Instr.IType Instr.Jump rd _ _ -> - modify $ \s -> s {stateRegFile = modifyRF rd (pure res) (stateRegFile s)} - Instr.UType _ rd _ -> - modify $ \s -> s {stateRegFile = modifyRF rd (pure res) (stateRegFile s)} - Instr.IType (Instr.Env Instr.Call) _ _ _ -> do - modify $ \s -> s {stateRegFile = modifyRF 10 input (stateRegFile s)} - modify $ \s -> s {stateWbRegFwd = pure (10, unAccess input)} - _ -> pure () - -pipe :: LeakM () -pipe = withCtrlReset $ do - writeback - memory - execute - decode - fetch - where - withCtrlReset m = do - firstCycle <- gets stateFirstCycle - modify $ \s -> - s - { stateFirstCycle = firstCycle, - stateJumpAddr = Nothing, - stateDeLoadHazard = Nothing, - stateDeCall = False, - stateMeMemInstr = False, - stateMeRegFwd = Nothing, - stateWbRegFwd = Nothing - } - void m - modify $ \s -> s {stateFirstCycle = False} - -circuit :: State -> Input Identity -> (State, Out) -circuit = flip $ execRWS pipe diff --git a/src/Leak/PC/PC.hs b/src/Leak/PC/PC.hs deleted file mode 100644 index 2e5cd6e..0000000 --- a/src/Leak/PC/PC.hs +++ /dev/null @@ -1,188 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} --- touch to force rebuild - -module Leak.PC.PC - ( obs, - leak, - sim, - circuit, - proj, - Leak.PC.PC.simulator, - runSimulator, - watchSim, - pcsEqual, - implementation, - -- comment them out to disable Pantomime checks for faster compilation - -- theory, - -- circuits, - -- tickStateCorrespondence, - -- projectionCoherence, - ) -where - -import Access -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad -import Control.Monad.RWS -import Control.Monad.State -import Core (Input (..), MemAccess (..), Output (..), initInput) -import qualified Core -import Data.Bifunctor (second) -import Data.Functor.Identity -import Data.Monoid -import qualified Instruction as Instr -import qualified Leak.PC.Leak as Leak -import qualified Leak.PC.Sim as Sim -import qualified Simulate -import Memory.Types -import Memory.Vec () -import Types -import Util -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -stateless :: (a -> b) -> () -> a -> ((), b) -stateless f _ x = ((), f x) - -implementation :: Core.State Identity -> Input Identity -> (Core.State Identity, Output Identity) -implementation = Core.circuit - -obs :: () -> Output Identity -> ((), Maybe Address) -obs = stateless obs' - -obs' :: Output Identity -> Maybe Address -obs' o_sim = do - mem <- outMem o_sim - guard $ memIsInstr mem - pure $ memAddress mem - -leak :: Leak.State -> Input Identity -> (Leak.State, Leak.Out) -leak = Leak.circuit - -sim :: Sim.State -> Leak.Out -> (Sim.State, Maybe Address) -sim ss l_out = - let (ss', addr) = Sim.circuit ss l_out - in (ss', join (getFirst addr)) - -circuit :: - (Leak.State, Sim.State) -> - Input Identity -> - ((Leak.State, Sim.State), Maybe Address) -circuit (ts, ss) i = ((ts', ss'), addr) - where - (ts', o_leak) = leak ts i - (ss', addr) = sim ss o_leak - -proj :: Core.State Identity -> (Leak.State, Sim.State) -proj s = (ts, ss) - where - ts = - Leak.State - { Leak.stateFePc = Core.stateFePc s, - Leak.stateDePc = Core.stateDePc s, - Leak.stateDeExpInstr = Core.stateDeExpInstr s, - Leak.stateExPc = Core.stateExPc s, - Leak.stateExInstr = Core.stateExInstr s, - Leak.stateMemInstr = Core.stateMeInstr s, - Leak.stateMemRes = unAccess $ Core.stateMeRes s, - Leak.stateMemVal = pack $ Core.stateMeAddr s, -- this is wrong, I am just making it compile - Leak.stateWbInstr = Core.stateWbInstr s, - Leak.stateWbRes = unAccess $ Core.stateWbRes s, - Leak.stateRegFile = Core.stateRegFile s, - Leak.stateMeMemInstr = Core.ctrlMeMemInstr $ Core.stateCtrl s, - Leak.stateHalt = Core.stateHalt s, - Leak.stateMeRegFwd = fmap (second unAccess) $ Core.ctrlMeRegFwd $ Core.stateCtrl s, - Leak.stateWbRegFwd = fmap (second unAccess) $ Core.ctrlWbRegFwd $ Core.stateCtrl s, - Leak.stateJumpAddr = Core.ctrlExJumpAddr $ Core.stateCtrl s, - Leak.stateDeLoadHazard = Core.ctrlDeLoadHazard $ Core.stateCtrl s, - Leak.stateDeCall = False, - Leak.stateFirstCycle = False - } - ss = - Sim.State - { Sim.stateFePc = Core.stateFePc s, - Sim.stateDePc = Core.stateDePc s, - Sim.stateExPc = Core.stateExPc s, - Sim.stateExInstr = toLeakInstr $ Core.stateExInstr s, - Sim.stateMemInstr = killJump $ toLeakInstr $ Core.stateMeInstr s, - Sim.stateWbInstr = killJump $ toLeakInstr $ Core.stateWbInstr s, - Sim.stateHalt = Core.stateHalt s, - Sim.stateHaltNextPc = Core.stateHaltNextPc s, - Sim.stateMeMemInstr = Core.ctrlMeMemInstr $ Core.stateCtrl s, - Sim.stateJumpAddr = Core.ctrlExJumpAddr $ Core.stateCtrl s, - Sim.stateDeLoadHazard = Core.ctrlDeLoadHazard $ Core.stateCtrl s, - Sim.stateDeCall = False, - Sim.stateFirstCycle = False - } - - killJump :: Leak.Instr -> Leak.Instr - killJump (Leak.Instr Leak.Jump _) = Leak.nop - killJump i = i - - toLeakInstr :: Instr.Instruction -> Leak.Instr - toLeakInstr instr = - Leak.Instr - (Leak.mkInstr instr) - (Leak.mkDeps instr) - -simulator :: - forall m. - (MonadState ((Core.State Identity, Output Identity), Simulate.Mem MEM_SIZE_BYTES) m) => - CircuitSim m (Input Identity) (Leak.State, Sim.State) (Maybe Address, Maybe Address) -simulator = - CircuitSim - { circuitInput = initInput, - circuitState = (Leak.init, Sim.init), - circuitStep = step, - circuitNext = next - } - where - step :: - Input Identity -> - (Leak.State, Sim.State) -> - m ((Leak.State, Sim.State), (Maybe Address, Maybe Address)) - step i (ts, ss) = do - ((s_core_old, _), mem) <- get - let (s_core', o_core) = implementation s_core_old i - - -- Update memory manually (register file is now in s_core') - let mem' = case outMem o_core of - Just (MemAccess _ addr size (Just val)) -> - mem {Simulate.memRAM = write size addr (runIdentity val) (Simulate.memRAM mem)} - _ -> mem - - put ((s_core', o_core), mem') - - let ((ts', ss'), addr) = circuit (ts, ss) i - pure ((ts', ss'), (obs' o_core, addr)) - - next :: (Leak.State, Sim.State) -> (Maybe Address, Maybe Address) -> m (Maybe (Input Identity)) - next _ (_o, _addr_sim) = do - ((s_core, o_core), mem) <- get - let (mi, mem') = runState (circuitNext Simulate.simulator s_core o_core) mem - modify $ \(s, _mem) -> (s, mem') - pure mi - -runSimulator :: - ( CircuitSim - (State ((Core.State Identity, Output Identity), Simulate.Mem MEM_SIZE_BYTES)) - (Input Identity) - (Leak.State, Sim.State) - (Maybe Address, Maybe Address) -> - State ((Core.State Identity, Output Identity), Simulate.Mem MEM_SIZE_BYTES) a - ) -> - Vec PROG_SIZE Word -> - a -runSimulator f prog = evalState (f Leak.PC.PC.simulator) s - where - s = ((Core.init, mempty), Simulate.Mem (mkRAM' prog)) - mkRAM' p = Memory.Types.mkRAM @PROG_SIZE @RAM_SIZE_BYTES p - -watchSim :: - Vec PROG_SIZE Word -> - [((Leak.State, Sim.State), (Maybe Address, Maybe Address), Maybe (Input Identity))] -watchSim = runSimulator watch - -pcsEqual :: Vec PROG_SIZE Word -> Bool -pcsEqual = all check . watchSim - where - check (_, (o, o'), _) = o == o' diff --git a/src/Leak/PC/Sim.hs b/src/Leak/PC/Sim.hs deleted file mode 100644 index 7309aaf..0000000 --- a/src/Leak/PC/Sim.hs +++ /dev/null @@ -1,240 +0,0 @@ -module Leak.PC.Sim - ( pipe, - circuit, - init, - State (..), - ) -where - -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad -import Control.Monad.RWS -import qualified Core as AimCore -import qualified Instruction as Instr -import Data.Maybe (fromMaybe, isJust, isNothing) -import Data.Monoid -import qualified Leak.PC.Leak as Leak -import Memory.Types -import Types -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - -data State = State - { stateFePc :: Address, - stateDePc :: Address, - stateExPc :: Address, - stateExInstr :: Leak.Instr, - stateMemInstr :: Leak.Instr, - stateWbInstr :: Leak.Instr, - stateJumpAddr :: Maybe Address, - stateMeMemInstr :: Bool, - stateHalt :: Maybe AimCore.HaltState, - stateHaltNextPc :: Address, - stateDeLoadHazard :: Maybe Address, - stateDeCall :: Bool, - stateFirstCycle :: Bool - } - deriving (Show, Eq) - -init ::State -init = - State - { stateFePc = initPc, - stateDePc = 0, - stateExPc = 0, - stateExInstr = Leak.nop, - stateMemInstr = Leak.nop, - stateWbInstr = Leak.nop, - stateHalt = Nothing, - stateHaltNextPc = 0, - stateMeMemInstr = False, - stateJumpAddr = Nothing, - stateDeLoadHazard = Nothing, - stateDeCall = False, - stateFirstCycle = True - } - -type SimM = RWS Leak.Out (First (Maybe Address)) State - -outputPc :: Address -> SimM () -outputPc addr = - tell $ pure $ pure addr - -outputNothing :: SimM () -outputNothing = tell $ pure Nothing - -fetch :: SimM () -fetch = do - pc <- gets stateFePc - mJumpAddr <- gets stateJumpAddr - deLoadHazard <- gets stateDeLoadHazard - deCall <- gets stateDeCall - meMemInstr <- gets stateMeMemInstr - status <- gets stateHalt - pending <- gets stateHaltNextPc - - let isHalted = isJust status || pending /= 0 - - unless (meMemInstr || isHalted) $ - outputPc pc - - let stall = deCall || meMemInstr || isHalted - - let next_pc = - fromMaybe - (fromMaybe - (if stall then pc else pc + 4) - deLoadHazard) - mJumpAddr - - modify $ \s -> - s - { stateFePc = next_pc, - stateDePc = if stall then stateDePc s else pc - } - -decode :: SimM () -decode = do - instr <- fromMaybe (Leak.Instr (Leak.Nop Instr.MemoryBusBusy) (Nothing, Nothing)) . getFirst <$> asks Leak.outInstr - - exInstr <- gets stateExInstr - mJumpAddr <- gets stateJumpAddr - firstCycle <- gets stateFirstCycle - status <- gets stateHalt - pending <- gets stateHaltNextPc - - let branch_first_cycle = isNopBranchFirstCycle exInstr - let load_hazard_first_cycle = isNopLoadHazardFirstCycle exInstr - let call_current_cycle = isCall exInstr - let halt_pending = pending /= 0 - - -- In Sim, we don't have the real instruction, but we know if it was stalled. - let load_hazard_current_cycle = case instrBase instr of - Leak.Nop Instr.LoadHazardFirstCycle -> True - _ -> Leak.loadHazard instr exInstr - - let ir' = - -- If a branch was taken in this cycle, we stall. - if isJust mJumpAddr then Leak.Instr (Leak.Nop Instr.JumpFirstCycle) (Nothing, Nothing) - -- If a branch was taken in the previous cycle, we stall. - else if branch_first_cycle then Leak.Instr (Leak.Nop Instr.JumpSecondCycle) (Nothing, Nothing) - -- If there is a load hazard with the instruction executed in this cycle, we stall. - else if load_hazard_current_cycle then Leak.Instr (Leak.Nop Instr.LoadHazardFirstCycle) (Nothing, Nothing) - -- If there was a load hazard in the previous cycle, we stall. - else if load_hazard_first_cycle then Leak.Instr (Leak.Nop Instr.LoadHazardSecondCycle) (Nothing, Nothing) - -- If a syscall is executed in this cycle, we stall. - else if call_current_cycle then Leak.Instr (Leak.Nop Instr.Halted) (Nothing, Nothing) - -- If the core is not running anymore, we halt. - else if isJust status || halt_pending then Leak.Instr (Leak.Nop Instr.Halted) (Nothing, Nothing) - -- If this is the first cycle, the instruction to decode is gibberish from memory. - else if firstCycle then Leak.Instr (Leak.Nop Instr.FirstCycle) (Nothing, Nothing) - -- Otherwise we process the instruction from leakage. - else instr - - when (instrBase ir' == Leak.Nop Instr.Halted) $ - modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} - - when load_hazard_current_cycle $ do - pc <- gets stateDePc - modify $ \s -> s {stateDeLoadHazard = Just pc} - - when (isCall ir') $ - modify $ \s -> s {stateDeCall = True} - - modify $ \s -> - s - { stateExInstr = ir', - stateExPc = stateDePc s - } - where - instrBase (Leak.Instr b _) = b - isNopBranchFirstCycle (Leak.Instr (Leak.Nop Instr.JumpFirstCycle) _) = True - isNopBranchFirstCycle _ = False - isNopLoadHazardFirstCycle (Leak.Instr (Leak.Nop Instr.LoadHazardFirstCycle) _) = True - isNopLoadHazardFirstCycle _ = False - isCall (Leak.Instr Leak.Call _) = True - isCall _ = False - -execute :: SimM () -execute = do - instr <- gets stateExInstr - mjmpAddr <- getFirst <$> asks Leak.outJumpAddr - mBranchTaken <- getFirst . Leak.outBranchTaken <$> ask - mJumpValid <- getFirst . Leak.outJumpAddrValid <$> ask - - case Leak.instrBase instr of - Leak.Break -> do - pc <- gets stateExPc - modify $ \s -> - s - { stateJumpAddr = Nothing, - stateHaltNextPc = pc + 4, - stateMemInstr = killJump instr - } - _ -> do - modify $ \s -> - s - { stateJumpAddr = mjmpAddr, - stateMemInstr = killJump instr - } - case Leak.instrBase instr of - Leak.Jump -> - when (isNothing mjmpAddr && isNothing mJumpValid) $ - modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} - Leak.Branch -> - when (isNothing mBranchTaken) $ - modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} - _ -> pure () - where - dummy = () - -memory :: SimM () -memory = do - instr <- gets stateMemInstr - modify $ \s -> s {stateWbInstr = killJump instr} - - mMeMemInstr <- getFirst . Leak.outMeMemInstr <$> ask - case mMeMemInstr of - Just True -> modify (\s -> s {stateMeMemInstr = True}) >> outputNothing - Just False -> modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} - Nothing -> pure () - -killJump :: Leak.Instr -> Leak.Instr -killJump (Leak.Instr Leak.Jump _) = Leak.nop -killJump i = i - -writeback :: SimM () -writeback = do - instr <- gets stateWbInstr - halted <- gets stateHalt - - pending <- gets stateHaltNextPc - when (pending /= 0) $ - modify $ \s -> s {stateHalt = Just (AimCore.EBreak pending), stateHaltNextPc = 0} - - mLeakedHalt <- getFirst . Leak.outHalt <$> ask - when (isJust halted || isJust mLeakedHalt) $ - outputNothing - -pipe :: SimM () -pipe = withCtrlReset $ do - writeback - memory - execute - decode - fetch - where - withCtrlReset m = do - firstCycle <- gets stateFirstCycle - modify $ \s -> - s - { stateFirstCycle = firstCycle, - stateJumpAddr = Nothing, - stateDeLoadHazard = Nothing, - stateDeCall = False, - stateMeMemInstr = False - } - void m - modify $ \s -> s {stateFirstCycle = False} - -circuit :: State -> Leak.Out -> (State, First (Maybe Address)) -circuit = flip $ execRWS pipe diff --git a/src/Leak/PCWithState/PCWithState.hs b/src/Leak/PCWithState/PCWithState.hs deleted file mode 100644 index bc64399..0000000 --- a/src/Leak/PCWithState/PCWithState.hs +++ /dev/null @@ -1,391 +0,0 @@ -module Leak.PCWithState.PCWithState () where - --- import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) --- import Control.Monad --- import Control.Monad.RWS --- import Control.Monad.State --- import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust) --- import Data.Monoid --- import Data.Set (Set) --- import qualified Data.Set as S --- import Data.Tuple (swap) --- import Debug.Trace --- import GHC.TypeNats --- import Instruction hiding (decode, halt) --- import qualified Instruction --- import Pipe --- import Regfile --- import qualified Simulate --- import Types --- import Util --- import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) --- --- data BaseLeakInst --- = LJ Address --- | LLoad RegIdx --- | LStore --- | LOther --- | LHalt --- deriving (Eq, Ord, Show) --- ----- | Instructions passed to the Simulator --- data LeakInst = LeakInst --- { leakBaseInst :: BaseLeakInst, --- leakDeps :: Set RegIdx --- -- Debugging fields --- -- leakOgInst :: Instruction, --- -- leakDePc :: Address --- } --- deriving (Eq, Show) --- --- data LeakState = LeakState --- { leakRF :: Regfile, --- leakRAM :: Vec MEM_SIZE_BYTES Byte, --- leakPc :: Address, --- leakStall :: Int --- } --- deriving (Eq, Show) --- --- leakNop :: LeakInst --- leakNop = LeakInst LOther mempty -- Instruction.nop 0 --- --- initLeak :: Vec PROG_SIZE Word -> LeakState --- initLeak prog = --- LeakState --- { leakRF = initRF, --- leakRAM = mkRAM prog, --- leakPc = initPc, --- leakStall = 0 --- } --- --- mkInst :: Instruction -> BaseLeakInst -> LeakInst --- mkInst inst leakInst = --- LeakInst --- { leakBaseInst = leakInst, --- leakDeps = S.fromList $ catMaybes [getRs1 inst, getRs2 inst] --- -- leakOgInst = inst, --- -- leakDePc = pc --- } --- --- type LeakM = State LeakState --- --- leak :: Input -> LeakM LeakInst --- leak input --- | not (inputIsInst input) = pure leakNop --- | otherwise = --- unlessStall $ do --- let mkInst' = mkInst inst --- inst' <- case inst of --- RType op rd r1 r2 -> do --- writeRF rd =<< alu op <$> readRF r1 <*> readRF r2 --- pure $ mkInst' LOther --- IType iop rd r1 imm -> do --- let op = --- case iop of --- Arith op' -> op' --- _ -> ADD --- res <- alu op <$> readRF r1 <*> pure (signExtend imm) --- case iop of --- Arith {} -> do --- writeRF rd res --- pure $ mkInst' LOther --- Load size sign -> do --- let loadExtend = \case --- (Byte, Signed) -> signExtend $ slice d7 d0 res --- (Byte, Unsigned) -> zeroExtend $ slice d7 d0 res --- (Half, Signed) -> signExtend $ slice d15 d0 res --- (Half, Unsigned) -> signExtend $ slice d15 d0 res --- (Word, _) -> signExtend $ slice d31 d0 res --- val = loadExtend (size, sign) --- writeRF rd =<< readRAM (unpack val) --- pure $ mkInst' $ LLoad rd --- Jump -> do --- writeRF rd =<< (bitCoerce . (+ 4)) <$> gets leakPc --- pure $ mkInst' $ LJ $ bitCoerce res --- Env {} -> error "" --- SType size imm r1 r2 -> do --- addr <- unpack <$> (alu ADD <$> readRF r1 <*> pure (signExtend imm)) --- val <- readRF r2 --- writeRAM size addr val --- pure $ mkInst' LStore --- BType cmp imm r1 r2 -> do --- branched <- branch cmp <$> readRF r1 <*> readRF r2 --- if branched --- then --- mkInst' . LJ . bitCoerce --- <$> (alu ADD <$> (bitCoerce <$> gets leakPc) <*> pure (signExtend imm)) --- else pure $ mkInst' LOther --- UType Zero rd imm -> do --- let imm' = imm ++# 0 `shiftL` 12 --- writeRF rd $ imm' --- pure $ mkInst' LOther --- UType PC rd imm -> do --- let imm' = imm ++# 0 `shiftL` 12 --- writeRF rd imm' --- pure $ mkInst' LOther --- JType rd imm -> do --- writeRF rd =<< (bitCoerce . (+ 4)) <$> gets leakPc --- mkInst' . LJ . bitCoerce --- <$> (alu ADD <$> (bitCoerce <$> gets leakPc) <*> pure (signExtend imm)) --- EBREAK -> --- pure $ mkInst' LHalt --- _ -> --- pure leakNop --- case leakBaseInst inst' of --- LJ pc' -> modify $ \s -> --- s --- { leakPc = pc', --- leakStall = leakStall s + 2 --- } --- LLoad {} -> modify $ \s -> s {leakStall = leakStall s + 1} --- _ -> modify $ \s -> s {leakPc = leakPc s + 4} --- --- pure inst' --- where --- inst = Instruction.decode $ inputMem input --- unlessStall m = do --- stall <- gets leakStall --- if (stall > 0) --- then do --- modify $ \s -> s {leakStall = stall - 1} --- pure leakNop --- else m --- --- leakRun :: LeakState -> Input -> (LeakState, LeakInst) --- leakRun s i = swap $ runState (leak i) s --- --- readRF :: RegIdx -> LeakM Word --- readRF idx = gets $ lookupRF idx . leakRF --- --- writeRF :: RegIdx -> Word -> LeakM () --- writeRF idx val = --- modify $ \s -> s {leakRF = modifyRF idx val $ leakRF s} --- --- writeRAM :: Size -> Address -> Word -> LeakM () --- writeRAM size addr w = --- modify $ \s -> s {leakRAM = write size addr w $ leakRAM s} --- --- readRAM :: Address -> LeakM Word --- readRAM addr = gets $ readWord addr . leakRAM --- --- type SimM = RWS LeakInst (First (Maybe Address)) SimState --- --- stall :: [Stage] -> SimM () --- stall stages = --- modify $ \s -> s {simStall = simStall s <> S.fromList stages} --- --- stallingM :: Stage -> SimM Bool --- stallingM stage = --- S.member stage <$> gets simStall --- --- outputPC :: Address -> SimM () --- outputPC addr = --- tell $ pure $ pure addr --- --- outputNothing :: SimM () --- outputNothing = tell $ pure Nothing --- --- data Stage = Fe | De | Ex | Mem | Wb --- deriving (Show, Eq, Ord) --- --- data SimState = SimState --- { simFePc :: Address, --- simDePc :: Address, --- simExPc :: Address, --- simJumpAddr :: Maybe Address, --- simExInstr :: LeakInst, --- simExRes :: Word, --- simMemInstr :: LeakInst, --- simMemRes :: Word, --- simWbInstr :: LeakInst, --- simStall :: Set Stage, --- simHalt :: Bool --- } --- deriving (Show) --- --- initSim :: SimState --- initSim = --- SimState --- { simFePc = initPc, --- simDePc = 0, --- simExPc = 0, --- simJumpAddr = Nothing, --- simExInstr = leakNop, --- simExRes = 0, --- simMemInstr = leakNop, --- simMemRes = 0, --- simWbInstr = leakNop, --- simStall = mempty, --- simHalt = False --- } --- --- simFetch :: SimM () --- simFetch = do --- s <- get --- stalling <- stallingM Fe --- unless stalling $ do --- modify $ \s -> --- s --- { simFePc = fromMaybe (simFePc s + 4) (simJumpAddr s), --- simDePc = simFePc s --- } --- outputPC $ simFePc s --- --- simDecode :: SimM () --- simDecode = do --- s <- get --- instr <- ask --- when (isLoad instr) $ --- stall [Fe] --- ex_ir <- gets simExInstr --- when (loadHazard instr ex_ir) $ --- stall [De] --- stalling <- stallingM De --- modify $ \s -> --- s --- { simExInstr = --- if stalling --- then leakNop --- else instr, --- simExPc = simDePc s --- } --- where --- isLoad :: LeakInst -> Bool --- isLoad (LeakInst LLoad {} _) = True --- isLoad _ = False --- --- loadHazard :: LeakInst -> LeakInst -> Bool --- loadHazard de_ir ex_ir@(LeakInst (LLoad rd) _) = --- any (== rd) $ S.toList $ leakDeps de_ir --- loadHazard _ _ = False --- --- simExecute :: SimM () --- simExecute = do --- instr <- gets simExInstr --- case leakBaseInst instr of --- LJ addr -> do --- stall [De] --- modify $ \s -> s {simJumpAddr = pure addr} --- _ -> pure () --- --- modify $ \s -> s {simMemInstr = instr} --- --- simMemory :: SimM () --- simMemory = do --- instr <- gets simMemInstr --- case leakBaseInst instr of --- LLoad _ -> do --- outputNothing --- stall [Fe] --- LStore -> do --- outputNothing --- stall [Fe] --- LJ {} -> --- stall [De] --- _ -> pure () --- --- modify $ \s -> s {simWbInstr = simMemInstr s} --- --- simWriteback :: SimM () --- simWriteback = do --- instr <- gets simWbInstr --- halted <- gets simHalt --- --- when halted $ --- outputNothing --- --- case leakBaseInst instr of --- LHalt -> do --- modify $ \s -> --- s --- { simMemInstr = leakNop, --- simExInstr = leakNop, --- simHalt = True --- } --- outputNothing --- LLoad {} -> stall [De] --- LStore -> stall [De] --- _ -> pure () --- --- simTick :: SimM () --- simTick = do --- modify $ \s -> s {simStall = mempty, simJumpAddr = empty} --- simWriteback --- simMemory --- simExecute --- simDecode --- simFetch --- --- simRun :: SimState -> LeakInst -> (SimState, Maybe Address) --- simRun s i = (fromMaybe Nothing . getFirst) <$> execRWS simTick i s --- --- simLeakRun :: --- Input -> --- (LeakState, SimState) -> --- ((LeakState, SimState), Maybe Address) --- simLeakRun input (ls, ss) = ((ls', ss'), addr) --- where --- (ls', simin) = leakRun ls input --- (ss', addr) = simRun ss simin --- --- simulator :: --- forall m. --- ( MonadState ((Pipe, Output), Simulate.Mem MEM_SIZE_BYTES) m --- ) => --- Vec PROG_SIZE Word -> --- CircuitSim m Input (LeakState, SimState) (Maybe Address, Maybe Address) --- simulator prog = --- CircuitSim --- { circuitInput = initInput, --- circuitState = (initLeak prog, initSim), --- circuitStep = step, --- circuitNext = next --- } --- where --- obs :: Output -> Maybe Address --- obs sim_o = do --- mem <- getFirst $ outMem sim_o --- guard $ memIsInst mem --- pure $ memAddress mem --- --- step :: --- Input -> --- (LeakState, SimState) -> --- m ((LeakState, SimState), (Maybe Address, Maybe Address)) --- step i s = do --- ((sim_s, _), mem) <- get --- let (sim_res@(_, sim_o), mem') = runState (circuitStep Simulate.simulator i sim_s) mem --- put (sim_res, mem') --- let (s', o) = simLeakRun i s --- pure (s', (o, obs sim_o)) --- --- next :: (Maybe Address, Maybe Address) -> m (Maybe Input) --- next (o, sim_addr) = do --- ((_, sim_o), mem) <- get --- let (mi, mem') = runState (circuitNext Simulate.simulator sim_o) mem --- modify $ \(s, _mem) -> (s, mem') --- pure mi --- --- runSimulator :: --- ( CircuitSim --- (State ((Pipe, Output), Simulate.Mem MEM_SIZE_BYTES)) --- Input --- (LeakState, SimState) --- (Maybe Address, Maybe Address) -> --- State ((Pipe, Output), Simulate.Mem MEM_SIZE_BYTES) a --- ) -> --- Vec PROG_SIZE Word -> --- a --- runSimulator f prog = evalState (f $ simulator prog) $ mkS prog --- where --- mkS prog = ((initPipe, mempty), Simulate.Mem (mkRAM prog) initRF) --- --- watchSim :: --- Vec PROG_SIZE Word -> --- [((LeakState, SimState), (Maybe Address, Maybe Address), Maybe Input)] --- watchSim = runSimulator watch --- --- pcsEqual :: Vec PROG_SIZE Word -> Bool --- pcsEqual = all check . watchSim --- where --- check (_, (o, o'), _) = o == o' diff --git a/src/Leak/SecretPC/Leak.hs b/src/Leak/SecretPC/Leak.hs deleted file mode 100644 index 9b110c8..0000000 --- a/src/Leak/SecretPC/Leak.hs +++ /dev/null @@ -1,36 +0,0 @@ -{-# LANGUAGE StandaloneDeriving #-} - -module Leak.SecretPC.Leak - ( circuit, - init, - In, - Out, - State, - ) -where - -import Access -import Core (Input (..)) -import Data.Functor.Identity -import Prelude hiding (Word, init) - -type In = Input PubSec - -type State = () - -type Out = Input PubSec - -deriving instance Eq Out - -circuit :: State -> In -> (State, Out) -circuit _ input = - ((), output) - where - output :: Out - output = - input - { inputMem = censor $ inputMem input - } - -init :: State -init = () diff --git a/src/Leak/SecretPC/PC.hs b/src/Leak/SecretPC/PC.hs deleted file mode 100644 index 50ae8f7..0000000 --- a/src/Leak/SecretPC/PC.hs +++ /dev/null @@ -1,148 +0,0 @@ -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE UndecidableInstances #-} - -module Leak.SecretPC.PC - ( obs, - leak, - sim, - circuit, - proj, - pcsEqual, - implementation, - -- comment them out to disable Pantomime checks for faster compilation - -- theory, - -- tickStateCorrespondence, - -- projectionCoherence, - ) -where - -import Access (PubSec(..), censor) -import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) -import Control.Monad (guard) -import Control.Monad.State -import Core (Control (..), Input (..), MemAccess (..), Output (..), initInput) -import qualified Core -import Data.Bifunctor (second) -import Data.Composition -import qualified Leak.Existence as Existence -import qualified Leak.SecretPC.Leak as Leak -import qualified Pantomime.Clash.NonInterference as P -import RegFile -import qualified Simulate -import Memory.Types -import Memory.Vec () -import Types -import Util -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) - - -type SimState = Core.State PubSec - -implementation :: Core.State PubSec -> Input PubSec -> (Core.State PubSec, Output PubSec) -implementation = Core.circuit - -circuits :: P.SimulatorExistNI (Core.State PubSec) () SimState (Input PubSec) Leak.Out (Maybe Address) -circuits = - P.SimulatorExistNI - { P.implementation = second obs' .: implementation, - P.leakage = leak, - P.projection = proj - } - -stateless :: (a -> b) -> () -> a -> ((), b) -stateless f _ x = ((), f x) - -obs :: () -> Output PubSec -> ((), Maybe Address) -obs = stateless obs' - -obs' :: Output PubSec -> Maybe Address -obs' o_sim = do - mem <- outMem o_sim - guard $ memIsInstr mem - pure $ memAddress mem - -leak :: () -> Input PubSec -> ((), Leak.Out) -leak = Leak.circuit - -sim :: SimState -> Leak.Out -> (SimState, Maybe Address) -sim = curry (Existence.simulatorFor circuits id) - -circuit :: - ((), SimState) -> - Input PubSec -> - (((), SimState), Maybe Address) -circuit (ts, ss) input = ((ts', ss'), addr) - where - (ts', o_leak) = leak ts input - (ss', addr) = sim ss o_leak - -proj' :: Core.State PubSec -> SimState -proj' s = - s - { Core.stateMeRes = censor (Core.stateMeRes s), - Core.stateWbRes = censor (Core.stateWbRes s), - Core.stateRegFile = let RegFile rf = Core.stateRegFile s in RegFile (Clash.Prelude.map censor rf), - Core.stateCtrl = - let c = Core.stateCtrl s - in c - { Core.ctrlMeRegFwd = second censor <$> Core.ctrlMeRegFwd c, - Core.ctrlWbRegFwd = second censor <$> Core.ctrlWbRegFwd c - } - } - -proj :: Core.State PubSec -> ((), SimState) -proj s = ((), proj' s) - -simulator :: - forall m. - (MonadState ((Core.State PubSec, Output PubSec), Simulate.Mem MEM_SIZE_BYTES) m) => - CircuitSim m (Input PubSec) (Leak.State, SimState) (Maybe Address, Maybe Address) -simulator = - CircuitSim - { circuitInput = initInput, - circuitState = (Leak.init, Core.init), - circuitStep = step, - circuitNext = next - } - where - step :: - Input PubSec -> - (Leak.State, SimState) -> - m ((Leak.State, SimState), (Maybe Address, Maybe Address)) - step i s = do - ((s_sim, _), mem) <- get - let (res_sim@(_, o_sim), mem') = runState (circuitStep Simulate.simulator i s_sim) mem - put (res_sim, mem') - let (s', o) = circuit s i - pure (s', (o, obs' o_sim)) - - next :: (Leak.State, SimState) -> (Maybe Address, Maybe Address) -> m (Maybe (Input PubSec)) - next _ (_o, _addr_sim) = do - ((s_sim, o_sim), mem) <- get - let (mi, mem') = runState (circuitNext Simulate.simulator s_sim o_sim) mem - modify $ \(s, _mem) -> (s, mem') - pure mi - -runSimulator :: - ( CircuitSim - (State ((Core.State PubSec, Output PubSec), Simulate.Mem MEM_SIZE_BYTES)) - (Input PubSec) - (Leak.State, SimState) - (Maybe Address, Maybe Address) -> - State ((Core.State PubSec, Output PubSec), Simulate.Mem MEM_SIZE_BYTES) a - ) -> - Vec PROG_SIZE Word -> - a -runSimulator f prog = evalState (f Leak.SecretPC.PC.simulator) s - where - s = ((Core.init, mempty), Simulate.Mem (mkRAM prog)) - -watchSim :: - Vec PROG_SIZE Word -> - [((Leak.State, SimState), (Maybe Address, Maybe Address), Maybe (Input PubSec))] -watchSim = runSimulator watch - -pcsEqual :: Vec PROG_SIZE Word -> Bool -pcsEqual = all check . watchSim - where - check (_, (o, o'), _) = o == o' diff --git a/test/Spec.hs b/test/Spec.hs index 92993a7..0392bb9 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -15,9 +15,6 @@ import Core import Data.Maybe (fromJust, isJust) import Instruction import InstructionSpec (instructionTests) -import qualified Leak.MonitorPC.PC as Leak.MonitorPC -import qualified Leak.PC.PC as Leak.PC -import qualified Leak.SecretPC.PC as Leak.SecretPC import RegFile import Simulate import Memory.Types @@ -35,7 +32,6 @@ import ProofSpec (proofTests) import Test.Tasty (TestTree, defaultMain, testGroup) import Test.Tasty.HUnit (assertBool, testCase, (@?=)) import Test.Tasty.QuickCheck -import TheoremSpec (nonInterferenceTheorem, simulatorTheorem) import "aimcore" Types import "aimcore" Util import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, undefined, (!!), (&&), (++), (||)) @@ -57,18 +53,6 @@ mkPureTest s (CPUTest prog expected) = in forM_ expected $ \(loc, res) -> readWord (fromIntegral loc) ram @?= res -mkPCLeakTest :: String -> Vec PROG_SIZE Word -> TestTree -mkPCLeakTest s prog = - testCase s $ - assertBool "" $ - Leak.PC.pcsEqual prog - -mkSecretPCLeakTest :: String -> Vec PROG_SIZE Word -> TestTree -mkSecretPCLeakTest s prog = - testCase s $ - assertBool "" $ - Leak.SecretPC.pcsEqual prog - #ifdef SMT_PROOF -- | The compile-time symbolic checks, read back out. -- @@ -158,50 +142,6 @@ tests = testExpected = [(0, sum [0 .. 10])] } ] - -- testGroup - -- "PC leak" - -- [ mkPCLeakTest "test 1" $ mkProg prog1, - -- mkPCLeakTest "test 2" $ mkProg prog1, - -- mkPCLeakTest "test 3" $ mkProg prog1 - -- {- - -- , testProperty "PC Simulator" $ - -- withMaxSuccess 500000 $ - -- simulatorTheorem - -- Leak.PC.proj - -- Leak.PC.leak - -- Leak.PC.sim - -- Core.circuit - -- Leak.PC.obs, - -- testProperty "Non-interference" $ - -- withMaxSuccess 500000 $ - -- nonInterferenceTheorem Leak.PC.proj Leak.PC.leak Core.circuit Leak.PC.obs - -- -} - -- ], - -- testGroup - -- "SecretPC leak" - -- [ mkSecretPCLeakTest "test 1" $ mkProg prog1, - -- mkSecretPCLeakTest "test 1" $ mkProg prog1, - -- mkSecretPCLeakTest "test 2" $ mkProg prog1, - -- mkSecretPCLeakTest "test 3" $ mkProg prog1, - -- mkSecretPCLeakTest "sumTo 10" $ mkProg $ sumTo 10 - -- {- - -- , testProperty "SecretPC Simulator" $ - -- withMaxSuccess 500000 $ - -- simulatorTheorem - -- Leak.SecretPC.proj - -- Leak.SecretPC.leak - -- Leak.SecretPC.sim - -- Core.circuit - -- Leak.SecretPC.obs, - -- testProperty "MonitorPC Non-interference" $ - -- withMaxSuccess 500000 $ - -- nonInterferenceTheorem - -- Leak.MonitorPC.proj - -- Leak.MonitorPC.leak - -- Core.circuit - -- Leak.MonitorPC.obs - -- -} - -- ] ], benchmarkTests ] diff --git a/test/TheoremSpec.hs b/test/TheoremSpec.hs deleted file mode 100644 index 18eebdc..0000000 --- a/test/TheoremSpec.hs +++ /dev/null @@ -1,201 +0,0 @@ -module TheoremSpec (simulatorTheorem, nonInterferenceTheorem) where - -import Test.Tasty.QuickCheck - -simulatorTheorem :: - ( Arbitrary input - , Arbitrary coreState - , Show input - , Show coreState - , Show leakState - , Show simState - , Show observable - , Show coreOutput - , Eq observable - , Eq leakState - , Eq simState - ) => - (coreState -> (leakState, simState)) -> -- proj - (leakState -> input -> (leakState, leakOut)) -> -- leak circuit - (simState -> leakOut -> (simState, observable)) -> -- sim circuit - (coreState -> input -> (coreState, coreOutput)) -> -- coreCircuit - (() -> coreOutput -> ((), observable)) -> -- obs - Gen Property -simulatorTheorem proj leakCircuit simCircuit coreCircuit obs = do - input <- arbitrary - s_core <- arbitrary - let (s_leak, s_sim) = proj s_core - (s_leak', o_leak) = leakCircuit s_leak input - (s_sim', observable_leaksim) = simCircuit s_sim o_leak - (s_core', o_core) = coreCircuit s_core input - (_, observable_core) = obs () o_core - pure $ - flip counterexample (observable_core == observable_leaksim && proj s_core' == (s_leak', s_sim')) $ - unlines - [ "input: ", - "-------------------------------", - show input, - "", - "s_core:", - "-------------------------------", - show s_core, - "", - "s_core':", - "-------------------------------", - show s_core', - "", - "s_leak:", - "-------------------------------", - show s_leak, - "", - "s_leak':", - "-------------------------------", - show s_leak', - "", - "s_sim:", - "-------------------------------", - show s_sim, - "", - "s_sim':", - "-------------------------------", - show s_sim', - "", - "proj s_core'", - "-------------------------------", - show $ proj s_core', - "", - "observable_leaksim:", - "-------------------------------", - show observable_leaksim, - "", - "observable_core:", - "-------------------------------", - show observable_core, - "", - "o_core:", - "-------------------------------", - show o_core - ] - --- | Logical implication: if p then q else True -implies :: Bool -> Bool -> Bool -implies p q = not p || q - --- | Non-interference theorem that doesn't require a simulator --- Based on the mathematical formulation with LeakStateConsistency and LeakOutputConsistency -nonInterferenceTheorem :: - ( Arbitrary input - , Arbitrary coreState - , Show input - , Show coreState - , Show leakState - , Show simState - , Show leakOut - , Show observable - , Eq leakState - , Eq simState - , Eq leakOut - , Eq observable - ) => - (coreState -> (leakState, simState)) -> -- proj - (leakState -> input -> (leakState, leakOut)) -> -- leak circuit - (coreState -> input -> (coreState, coreOutput)) -> -- impl circuit - (() -> coreOutput -> ((), observable)) -> -- obs circuit - Gen Property -nonInterferenceTheorem proj leak impl obs = do - -- Test LeakStateConsistency: impl-obs-proj-state ≡ leak-proj-state - input <- arbitrary - s <- arbitrary - sₒ <- arbitrary - - let -- Helper functions matching Agda code structure - implObsProjState (s, sₒ) i = - let (s', x) = impl s i - (sₒ', _) = obs sₒ x - (sₗ, _) = proj s' - in sₗ - - leakProjState (s, sₒ) i = - let (sₗ, _) = proj s - (sₗ', _) = leak sₗ i - in sₗ' - - implObsProjSo ((s, sₒ), i) = - let (s', x) = impl s i - (sₒ', o) = obs sₒ x - (sₗ, sₛ) = proj s' - in (sₛ, o) - - leakProjSo ((s, sₒ), i) = - let (sₗ, sₛ) = proj s - (sₗ', o) = leak sₗ i - in (sₛ, o) - - -- LeakStateConsistency - stateConsistency = implObsProjState (s, sₒ) input == leakProjState (s, sₒ) input - - -- Test LeakOutputConsistency: ∀ si si' → leak-proj-so si ≡ leak-proj-so si' → impl-obs-proj-so si ≡ impl-obs-proj-so si' - input2 <- arbitrary - s2 <- arbitrary - sₒ2 <- arbitrary - - let si = ((s, sₒ), input) - si' = ((s2, sₒ2), input2) - - -- LeakOutputConsistency: if leak outputs are equal, then impl outputs should be equal - outputConsistency = (leakProjSo si == leakProjSo si') `implies` (implObsProjSo si == implObsProjSo si') - - pure $ - flip counterexample (stateConsistency && outputConsistency) $ - unlines - [ "Non-interference theorem violation:", - "====================================", - "", - "State Consistency: " ++ show stateConsistency, - "Output Consistency: " ++ show outputConsistency, - "", - "input: ", - "-------------------------------", - show input, - "", - "s:", - "-------------------------------", - show s, - "", - "sₒ:", - "-------------------------------", - show sₒ, - "", - "implObsProjState result:", - "-------------------------------", - show $ implObsProjState (s, sₒ) input, - "", - "implObsProjState result:", - "-------------------------------", - show $ implObsProjState (s, sₒ) input, - "", - "leakProjState result:", - "-------------------------------", - show $ leakProjState (s, sₒ) input, - "", - "leakProjSo si:", - "-------------------------------", - show $ leakProjSo si, - "", - "leakProjSo si':", - "-------------------------------", - show $ leakProjSo si', - "", - "implObsProjSo si:", - "-------------------------------", - show $ implObsProjSo si, - "", - "implObsProjSo si':", - "-------------------------------", - show $ implObsProjSo si', - "", - "Second test case:", - "input2: " ++ show input2, - "s2: " ++ show s2, - "sₒ2: " ++ show sₒ2 - ] \ No newline at end of file From 37951dc0aced57b6f655ed3808160f41254f50fe Mon Sep 17 00:00:00 2001 From: Kristina Date: Mon, 12 Oct 2026 15:47:39 +0200 Subject: [PATCH 7/8] Use a single memory in the ST backend and run rv32ui-p-fence_i Memory.ST kept two copies of the program: fetches read a read-only map of the ELF segments, while loads and stores used a data array that loadElf also fills. A store to a code address therefore never reached later fetches, unlike in Memory.Vec, Memory.IO, the hardware RAM and the proof's memory model, all of which are a single memory. The core supports self-modifying code (that is what the store-hazard stall is for), so the benchmark backend was testing it against a memory it is not built for. Read fetches from the data array like every other access, and drop stProgram, readProgramWord and loadSTProgram; loadElf already copies every segment into the array. This re-enables rv32ui-p-fence_i, which was commented out in BenchmarkSpec because of the split, and adds it to IsaSpec, which had excluded it for the same stated reason although the ISA model has always used a single memory. It passes against both. 155 tests pass. Co-Authored-By: Claude Opus 5.5 --- src/Memory/ST.hs | 50 +++++++++---------------------------------- test/BenchmarkSpec.hs | 13 +++-------- test/IsaSpec.hs | 4 ++-- 3 files changed, 15 insertions(+), 52 deletions(-) diff --git a/src/Memory/ST.hs b/src/Memory/ST.hs index dc7e24e..a925b84 100644 --- a/src/Memory/ST.hs +++ b/src/Memory/ST.hs @@ -8,8 +8,6 @@ module Memory.ST runSTMemoryT, runSTSim, newSTMemory, - loadSTProgram, - readProgramWord, runUntilHalt, ) where @@ -21,10 +19,6 @@ import Control.Monad.Reader import Control.Monad.ST (RealWorld, ST, stToIO) import Core import Data.Array.ST (STUArray, newArray, readArray, writeArray) -import Data.ByteString (ByteString) -import qualified Data.ByteString as BS -import Data.Map.Strict (Map) -import qualified Data.Map.Strict as Map import Data.Word (Word8) import Memory.Types import Types @@ -32,11 +26,11 @@ import Util (CircuitSim (..), run1) import Prelude hiding (Ordering (..), Word, init, lines, not, undefined, (&&), (||)) import qualified Prelude as P --- | Separated memory state in ST. +-- | Memory state in ST: a single byte array that instruction fetches, loads +-- and stores all share, so a store to a code address is seen by later fetches +-- (as in "Memory.Vec", "Memory.IO" and the hardware RAM). data STMemory s = STMemory - { -- | Read-only program memory, indexed by address. - stProgram :: Map Address ByteString, - -- | Writable data memory array. + { -- | The memory array. stData :: STUArray s Address Word8, -- | Base address of the data array. stDataBase :: Address, @@ -52,15 +46,12 @@ runSTMemoryT :: STMemory s -> STMemoryT s m a -> m a runSTMemoryT mem (STMemoryT m) = runReaderT m mem instance {-# OVERLAPPING #-} (MonadIO m) => MonadMemory (STMemoryT RealWorld m) where - ramRead isInstr addr size = do + ramRead _isInstr addr size = do st <- ask - if isInstr - then pure $ readProgramWord addr (stProgram st) - else do - let offset = addr - stDataBase st - if offset < 0x1000000 && offset >= 0 - then liftIO $ stToIO $ readDataArray offset size (stData st) - else pure 0 + let offset = addr - stDataBase st + if offset < 0x1000000 && offset >= 0 + then liftIO $ stToIO $ readDataArray offset size (stData st) + else pure 0 ramWrite addr size w = do st <- ask let offset = addr - stDataBase st @@ -71,23 +62,6 @@ instance {-# OVERLAPPING #-} (MonadIO m) => MonadMemory (STMemoryT RealWorld m) markMemoryRegion _ _ _ = pure () isMemorySecret _ = pure False --- | Read a 32-bit word from the program segments. -readProgramWord :: Address -> Map Address ByteString -> Word -readProgramWord addr prog = - let b0 = readProgramByte addr - b1 = readProgramByte (addr + 1) - b2 = readProgramByte (addr + 2) - b3 = readProgramByte (addr + 3) - in b3 ++# b2 ++# b1 ++# b0 - where - readProgramByte a = case Map.lookupLE a prog of - Just (base, bs) -> - let offset = fromIntegral (a - base) - in if offset < BS.length bs - then bitCoerce (BS.index bs offset) - else 0 - Nothing -> 0 - -- | Read a sized value from the data array. readDataArray :: Address -> Size -> STUArray s Address Word8 -> ST s Word readDataArray addr size arr = case size of @@ -118,17 +92,13 @@ writeDataArray addr size w arr = case size of writeArray arr (addr + 2) (bitCoerce $ slice d23 d16 w) writeArray arr (addr + 3) (bitCoerce $ slice d31 d24 w) --- | Load segments into the STMemory program map (for W^X). -loadSTProgram :: forall s. STMemory s -> [(Address, ByteString)] -> ST s (STMemory s) -loadSTProgram st segments = pure $ st { stProgram = Map.fromList segments } - -- | Create a new STMemory. newSTMemory :: forall s. Address -> Address -> ST s (STMemory s) newSTMemory entry base = do -- Use a smaller 16MB array to start with, as RISC-V tests are small. let dataSize = 0x1000000 arr <- newArray (0, dataSize) 0 - pure $ STMemory Map.empty arr base entry + pure $ STMemory arr base entry -- | Run a simulation in the ST monad. runSTSim :: forall i s o a. (forall st. CircuitSim (ST st) i s o -> ST st a) -> CircuitSim (ST s) i s o -> ST s a diff --git a/test/BenchmarkSpec.hs b/test/BenchmarkSpec.hs index 1f06a2b..aec9f65 100644 --- a/test/BenchmarkSpec.hs +++ b/test/BenchmarkSpec.hs @@ -66,12 +66,10 @@ mkBenchmarkTest testName _benchmark = elf <- readElf (benchmarkPath _benchmark) entryOffset <- startAddr elf base <- baseAddr elf - let segments = getElfSegments elf - -- Run the simulator with STMemory and MonadMemory interface - stMem <- stToIO $ do - mem <- newSTMemory (fromIntegral entryOffset) (fromIntegral base) - loadSTProgram mem segments + -- Run the simulator with STMemory and MonadMemory interface; loadElf + -- copies the program's segments into memory. + stMem <- stToIO $ newSTMemory (fromIntegral entryOffset) (fromIntegral base) _ <- runSTMemoryT stMem $ do loadElf elf @@ -205,17 +203,12 @@ benchmarkTests = { benchmarkPath = "test/rv32ui/rv32ui-p-bne", benchmarkInstrument = testSuiteInstrument False }, - {- - -- Commented out because fence_i involves self-modifying code, - -- which is explicitly disallowed by the W^X (Write XOR Execute) - -- policy enforced in STMemory. mkBenchmarkTest "rv32ui-p-fence_i" BenchmarkTest { benchmarkPath = "test/rv32ui/rv32ui-p-fence_i", benchmarkInstrument = testSuiteInstrument False }, - -} mkBenchmarkTest "rv32ui-p-jal" BenchmarkTest diff --git a/test/IsaSpec.hs b/test/IsaSpec.hs index b32f427..29e7e57 100644 --- a/test/IsaSpec.hs +++ b/test/IsaSpec.hs @@ -109,8 +109,7 @@ mkIsaTest name = Left e -> assertFailure e -- | The same programs "BenchmarkSpec" runs against the core, run against the --- ISA model instead. @fence_i@ is excluded for the same reason it is excluded --- there: it is self-modifying code. +-- ISA model instead. isaConformanceTests :: TestTree isaConformanceTests = testGroup @@ -120,6 +119,7 @@ isaConformanceTests = programs = [ "add", "addi", "and", "andi", "auipc", "beq", "bge", "bgeu", "blt", "bltu", "bne", + "fence_i", "jal", "jalr", "lb", "lbu", "ld_st", "lh", "lhu", "lui", "lw", "ma_data", From 7863aa5d0ca4b2785d48db7e006cca10659d0c8a Mon Sep 17 00:00:00 2001 From: Kristina Date: Mon, 12 Oct 2026 16:06:47 +0200 Subject: [PATCH 8/8] Drop the unused instruction flag from MonadMemory.ramRead ramRead took a Bool saying whether the read was an instruction fetch. Memory.ST was the only backend that used it, to send fetches to its read-only program copy; now that every backend is a single memory, no instance looks at it. Remove it from the class, the Vec, IO and ST instances, and the two callers (Simulate and ElfLoader). The flag on the core's MemAccess stays: the leakage model's obsOf uses it to tell an instruction fetch from a data read on the bus. Full build with the smt-proof flag passes all symbolic properties; 155 tests pass. Co-Authored-By: Claude Opus 5.5 --- src/Elf/ElfLoader.hs | 2 +- src/Memory/IO.hs | 4 ++-- src/Memory/ST.hs | 2 +- src/Memory/Types.hs | 2 +- src/Memory/Vec.hs | 2 +- src/Simulate.hs | 4 ++-- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Elf/ElfLoader.hs b/src/Elf/ElfLoader.hs index d01cb38..82369bf 100644 --- a/src/Elf/ElfLoader.hs +++ b/src/Elf/ElfLoader.hs @@ -89,7 +89,7 @@ readStringFromMemory :: (MonadMemory m) => Unsigned 32 -> Unsigned 32 -> m Strin readStringFromMemory addr count = do bytes <- forM [0 .. count - 1] $ \i -> do - byte <- ramRead False (addr + i) Byte + byte <- ramRead (addr + i) Byte pure $ fromIntegral (byte .&. 0xFF) pure $ P.map chr $ takeWhile (/= 0) bytes diff --git a/src/Memory/IO.hs b/src/Memory/IO.hs index ada092d..4d54ff4 100644 --- a/src/Memory/IO.hs +++ b/src/Memory/IO.hs @@ -59,7 +59,7 @@ loadProgram :: (MonadMemory m) => Elf -> m () loadProgram elf = loadElf elf instance {-# OVERLAPPING #-} MonadMemory (IOMemT IO) where - ramRead _isInstr addr _size = do + ramRead addr _size = do ramArray <- asks ioMemRAM bytes <- forM [0 .. 3] $ \i -> do w8 <- lift $ readArray ramArray (fromIntegral addr + i) @@ -124,7 +124,7 @@ loadSecureProgram :: (MonadMemory m) => Elf -> m () loadSecureProgram elf = loadElf elf instance {-# OVERLAPPING #-} MonadMemory (SecureIOMemT IO) where - ramRead _isInstr addr _size = do + ramRead addr _size = do ramArray <- asks secureIOMemRAM bytes <- forM [0 .. 3] $ \i -> do w8 <- lift $ readArray ramArray (fromIntegral addr + i) diff --git a/src/Memory/ST.hs b/src/Memory/ST.hs index a925b84..963c3dd 100644 --- a/src/Memory/ST.hs +++ b/src/Memory/ST.hs @@ -46,7 +46,7 @@ runSTMemoryT :: STMemory s -> STMemoryT s m a -> m a runSTMemoryT mem (STMemoryT m) = runReaderT m mem instance {-# OVERLAPPING #-} (MonadIO m) => MonadMemory (STMemoryT RealWorld m) where - ramRead _isInstr addr size = do + ramRead addr size = do st <- ask let offset = addr - stDataBase st if offset < 0x1000000 && offset >= 0 diff --git a/src/Memory/Types.hs b/src/Memory/Types.hs index 8bcade2..abc5268 100644 --- a/src/Memory/Types.hs +++ b/src/Memory/Types.hs @@ -27,7 +27,7 @@ import Types import Prelude hiding (Ordering (..), Word, init, iterate, log, map, not, repeat, replicate, take, undefined, (!!), (&&), (++), (||)) class Monad m => MonadMemory m where - ramRead :: Bool -> Address -> Size -> m Word + ramRead :: Address -> Size -> m Word ramWrite :: Address -> Size -> Word -> m () -- | Mark a region of memory as public or secret markMemoryRegion :: Address -> Address -> Bool -> m () diff --git a/src/Memory/Vec.hs b/src/Memory/Vec.hs index d86a044..0d48b62 100644 --- a/src/Memory/Vec.hs +++ b/src/Memory/Vec.hs @@ -20,7 +20,7 @@ data Mem n = Mem deriving (Eq, Show, Generic, NFDataX) instance (KnownNat n, Monad m, MonadState (Mem n) m) => MonadMemory m where - ramRead _isInstr addr _size = readWord addr <$> gets memRAM + ramRead addr _size = readWord addr <$> gets memRAM ramWrite addr size w = do ram <- gets memRAM modify $ \s -> s {memRAM = write size addr w ram} diff --git a/src/Simulate.hs b/src/Simulate.hs index aa0d314..f2d336a 100644 --- a/src/Simulate.hs +++ b/src/Simulate.hs @@ -48,10 +48,10 @@ simulator = where doMemory :: m (f Word) doMemory - | Just (MemAccess isInstr addr size mval) <- mem = + | Just (MemAccess _ addr size mval) <- mem = case mval of Nothing -> do - word <- ramRead isInstr addr size + word <- ramRead addr size isSecret <- isMemorySecret addr pure (conditionalSecret isSecret word) Just val -> do