Repository navigation
Conversation
Forks on public branches, layered memory, and memcmp checks.
Code tables come from Template Haskell. Registers live in a tree.
fe25519_cswap and libgcc's __muldi3 leak.
Checks that the native decode matches decode'.
Cuts the proof-smt interface files from megabytes to kilobytes.
Rebuilds the benchmarks, recalibrates the stepper checks and pins symfc to the commit with SymFCWith.
SymFC now takes a list of embedding names. Pins symfc to 2784ac7.
Bitwuzla rejects the Int sort that SBV sends when a check expects a counterexample.
Each proof now draws its inputs with fresh and fails the build when it does not hold, so the results lists and the tests that read them are gone. bogus now expects a counterexample.
The stepper now sends shifts as bitvector shifts, as the hardware proofs do, so no query has an Int and all of them run under Bitwuzla. Z3 does not finish indStep3. Pins symfc to 4aee0d8, which fixes the crash this exposed.
The stepper now reports a leak only when leakOf can differ between the two runs, so its notion of a leak is the one the hardware proof uses, and LeakKind is gone. It skips the solver when the registers leakOf reads are the same in both runs, which leakOfReadsOnlyLeakOfReads proves sound. relStepMatchesIsaStepInBothRuns checks a step from two different runs against isaStep in each.
A run with a cold dependency cache took about 50 minutes.
The core no longer halts with SecurityViolation when a secret reaches a fetch, an address or a branch, so PubSec, fromPublic, noSecrets and the secure-memory mode are gone and Access only unwraps a value. The relational checker now decides leaks with leakOf, so the hardware leakage theorem only says that the bus trace is a function of the leakOf trace. The mark_memory_region syscall is kept as a no-op so the existing benchmark binaries still run.
With the secrecy methods gone, Access only unwrapped a value, which is what extract from Comonad already does. Access is now a constraint synonym, and unAccess is extract.
isaStepM is the step written once against Machine, the register and memory operations a step needs. isaStep runs it on one state, and relStep runs it on both runs at once, so the checker no longer has its own copy of the instruction semantics.
The checker reads instructions from a fixed table while isaStep reads them from memory, so a store into the code would make the two disagree. Such a store now ends the run with WritesCode instead of going unnoticed.
Each table word must be the word memReadWord gives at that address in the memory loadElf builds, or the splice fails. The FetchesByAddress proofs show that codeFetch finds exactly the table's addresses, each at its own address.
A word store at 0xfffffffe writes bytes 0 and 1, but writesCode compared the store's first and last byte with plain < and <=, so it missed the wrap and the store into the code went unreported. The overlap test now subtracts modulo 2^32. The invariant proof found this.
The step-match proofs started only from fresh states, with no fetch hint and no pending writes. relStepKeepsInvariant starts from the shape a state has after some steps: a fetch hint into a code table, a register written through an unknown index, pending word and byte writes, and a path condition. Every outcome must match isaStep in both runs and keep the code and the hint equal to memory. Two more proofs start at the last code word and with no hint. The path condition holds the steps the checker must follow: both runs hold the same code, leak the same and leave the code alone. Without it the checker stops at every symbolic step with Leaks or WritesCode, and the proof says nothing. relStepWrongHintFails is the negative control.
relStepMatchesIsaStepInBothRuns started from two unrelated runs, so for every instruction that reads a register into leakOf the checker reported a leak and the proof accepted it: it said nothing about loads, stores, branches or jalr. relStepKeepsInvariant covers them, since its path condition makes the runs leak the same. The swapped-runs control moves to the invariant proof.
benchmark/eval.py deletes the program proofs' compiled files, rebuilds them with Bitwuzla and prints each checker run's verdict and time, optionally as CSV. Each proof fails the build unless the checker returns the verdict its name states, so the table is only printed in full when every verdict holds.
…-1.0.22 # Conflicts: # app/Main.hs # package.yaml # proof-smt/Proof/Functional/Induction.hs # proof/Proof/Core/Functional/System.hs # proof/Proof/Core/Leakage/Model.hs # proof/Proof/Core/Leakage/Solver.hs # proof/Proof/SMT/Array.hs # proof/Proof/SMT/Logged.hs # src/Access.hs # src/Core.hs # src/Core/ISA.hs # src/Core/RegFile.hs # src/Elf/Syscall.hs # src/HardwareSim.hs # src/Memory/Vec.hs # src/Simulate.hs # test/Spec.hs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
WIP, close #22.
Implements BinSec inspired relational approach to catching side channels. We have
Relis an applicative that either contains a pair of values (representing two different potentially secret values in two executions) and a single value (representing values we know are the same across the two executions, i.e. public values).A sort-of FlyRow approach to memory is implemented with
RelMem:memBaseis the flat SMT Array that stores the constants like the program's instructions, etc.memWritesis a map from address to memory cells. When a write happens, if the address is constant (not symbolic), it will be stored in the map, otherwise tomemBasedirectly. When reading from a symbolic address, it flushes the map onto a copy of the array then does select, but this is rarely needed.Code is loaded into the source via TemplateHaskell. For example:
This generates: