AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › arm64-semantics/Arm64/Trusted/Syscalls › Random.leanTier 3 · arm64-semantics

Random.lean🔗

Tier 3 · arm64-semantics used by the symbolic proof 2 headline theorems depend on it 3 of 37 lines trusted source ↗

Trusted, reviewed with the engine. The AArch64 model in arm64-semantics is Tier 3: it is reviewed in its own repository (check-trust-guards). The declarations that the headline statements use are shown for completeness.

Entropy Syscalls

Re-exports Arm64.Trusted.Syscalls.Drivers.Random (drivers/char/random.c: getrandom) and defines the single-syscall dispatch table Syscall.randomTable and handler Syscall.random.

@[expose] public section
namespace Arm64
namespace Syscall

def randomTableL28–38 ↗#

Dispatch table for kernel randomness (getrandom).

def randomTable : List (BitVec 64 × (State → State)) := [(SYS_GETRANDOM, execGetrandom)]
1 declaration not shown (lines 32–33): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.random

end Syscall
end Arm64