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

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

Signals.lean🔗

Tier 3 · arm64-semantics used by the symbolic proof 2 headline theorems depend on it 8 of 42 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.

Signal and Abort Syscalls

Re-exports Arm64.Trusted.Syscalls.Kernel.Signal (tkill, tgkill, sigaltstack, rt_sigaction, rt_sigprocmask) and defines Syscall.signalsTable and Syscall.signals.

@[expose] public section
namespace Arm64
namespace Syscall

def signalsTableL28–43 ↗#

Dispatch table for synchronous signal and abort syscalls (tkill, tgkill, sigaltstack, rt_sigaction, rt_sigprocmask).

def signalsTable : List (BitVec 64 × (State → State)) := [(SYS_TKILL, execTkill), (SYS_TGKILL, execTgkill), (SYS_SIGALTSTACK, execSigaltstack), (SYS_RT_SIGACTION, execRtSigaction), (SYS_RT_SIGPROCMASK, execRtSigprocmask)]
1 declaration not shown (lines 37–38): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.signals

end Syscall
end Arm64