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

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

Exit.lean🔗

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

Linux Process Termination exit & exit_group Syscalls (Arm64.Trusted.Syscalls.Kernel.Exit)

  • Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).

  • Linux 7.3 Upstream Sources:

    • kernel/exit.c:1094 (SYSCALL_DEFINE1(exit, int, error_code) -> do_exit)

    • kernel/exit.c:1138 (SYSCALL_DEFINE1(exit_group, int, error_code) -> do_group_exit)

  • Purpose & Key Exports: SYS_EXIT (93), SYS_EXIT_GROUP (94), and execExit.

@[expose] public section
namespace Arm64

def SYS_EXITL28–29 ↗#

Linux AArch64 exit syscall number (__NR_exit = 93, include/uapi/asm-generic/unistd.h:258, kernel/exit.c:1094).

def SYS_EXIT : BitVec 64 := 93#64

def SYS_EXIT_GROUPL31–32 ↗#

Linux AArch64 exit_group syscall number (__NR_exit_group = 94, include/uapi/asm-generic/unistd.h:260, kernel/exit.c:1138).

def SYS_EXIT_GROUP : BitVec 64 := 94#64

def execExitL34–42 ↗#

exit(status) (__NR_exit = 93, kernel/exit.c:1094) and exit_group(status) (__NR_exit_group = 94, kernel/exit.c:1138).

  • [INTENTIONAL_SCOPE]: In the single-threaded process model, exit and exit_group have identical process-termination semantics (execExit stores the full 64-bit X0 in .Exited, and ProcessOutcome.ofState preserves code unmasked rather than masking with 0xff, so X0 = 256 gives exitCode = 256 where Linux reports status 0; specifications constrain the full 64-bit exitCode).

def execExit (s : State) : State := s.setStatus (.Exited (s.readReg64 Reg.x0))
end Arm64