Types.lean🔗

Declarations on this page (34)

ELF Process Types (Arm64.Trusted.Process.Types)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: Contiguous mapped byte regions (Snapshot.Region, Snapshot.cellAt), process-level environment inputs (AuxvTag, AuxvConfig, ProcessInit, ProcessInputs), parsed static ELF64 image (ElfImage), and observable process termination outcome (ProcessOutcome).
When to read: Read when writing or auditing whole-binary process specifications (ElfRunsTo, ElfCorrect, ElfSafe) or inspecting how argv, envp, stdin, initial files, and kernel/environment initialization choices (init : ProcessInit) are supplied to an ELF process.

@[expose] public section

namespace Arm64

structure Snapshot.RegionL32–40 ↗#

One contiguous mapped byte region: bytes at [start, start + bytes.length), all with perm. The prefix [start, start + nonAnonLen) (0 by default) is backed by an ELF file mapping (anon := false in Snapshot.loadCellAt, matching Linux fs/binfmt_elf.c elf_map vs anonymous vm_brk_flags tail).

structure Snapshot.Region where
  start      : BitVec 64
  perm       : Perm
  bytes      : List (BitVec 8)
  nonAnonLen : Nat := 0

def Snapshot.cellAtL42–47 ↗#

The permission and byte at a in the first region containing a, if any.

def Snapshot.cellAt (regions : List Snapshot.Region) (a : BitVec 64) :
    Option (Option Perm × BitVec 8) :=
  regions.findSome? fun r =>
    let i := (a - r.start).toNat
    if h : i < r.bytes.length then some (some r.perm, r.bytes[i]) else none

def Snapshot.loadCellAtL49–58 ↗#

Process-loader cell lookup: like Snapshot.cellAt, clearing lazyFree := false and marking bytes in the file-backed prefix i < r.nonAnonLen with anon := false.

def Snapshot.loadCellAt (regions : List Snapshot.Region) (a : BitVec 64) :
    Option (Option Perm × BitVec 8) :=
  regions.findSome? fun r =>
    let i := (a - r.start).toNat
    if h : i < r.bytes.length then
      let p := { r.perm with lazyFree := false, anon := if i < r.nonAnonLen then false else r.perm.anon }
      some (some p, r.bytes[i])
    else none

end Arm64

namespace Arm64.Process

namespace AuxvTag

def nullL68–69 ↗#

End of auxiliary vector (AT_NULL = 0).

def null : BitVec 64 := 0#64

def phdrL70–71 ↗#

Address of program headers in memory (AT_PHDR = 3).

def phdr : BitVec 64 := 3#64

def phentL72–73 ↗#

Size in bytes of one program header entry (AT_PHENT = 4).

def phent : BitVec 64 := 4#64

def phnumL74–75 ↗#

Number of program header entries (AT_PHNUM = 5).

def phnum : BitVec 64 := 5#64

def pageszL76–77 ↗#

System page size in bytes (AT_PAGESZ = 6, 4096 on AArch64).

def pagesz : BitVec 64 := 6#64

def baseL78–79 ↗#

Base address of interpreter (AT_BASE = 7, 0 for static binaries).

def base : BitVec 64 := 7#64

def flagsL80–81 ↗#

Flags (AT_FLAGS = 8, 0).

def flags : BitVec 64 := 8#64

def entryL82–83 ↗#

Entry point of executable (AT_ENTRY = 9).

def entry : BitVec 64 := 9#64

def uidL84–85 ↗#

Real user ID (AT_UID = 11).

def uid : BitVec 64 := 11#64

def euidL86–87 ↗#

Effective user ID (AT_EUID = 12).

def euid : BitVec 64 := 12#64

def gidL88–89 ↗#

Real group ID (AT_GID = 13).

def gid : BitVec 64 := 13#64

def egidL90–91 ↗#

Effective group ID (AT_EGID = 14).

def egid : BitVec 64 := 14#64

def platformL92–93 ↗#

Address of platform string "aarch64\0" (AT_PLATFORM = 15).

def platform : BitVec 64 := 15#64

def hwcapL94–95 ↗#

CPU feature bitmask (AT_HWCAP = 16).

def hwcap : BitVec 64 := 16#64

def clktckL96–97 ↗#

Frequency of times() (AT_CLKTCK = 17, 100 Hz).

def clktck : BitVec 64 := 17#64

def secureL98–99 ↗#

Boolean secure-execution mode flag (AT_SECURE = 23, 0 for normal execution).

def secure : BitVec 64 := 23#64

def randomL100–101 ↗#

Address of 16 bytes of random seed data (AT_RANDOM = 25).

def random : BitVec 64 := 25#64

def hwcap2L102–103 ↗#

Extended CPU feature bitmask (AT_HWCAP2 = 26).

def hwcap2 : BitVec 64 := 26#64

def execfnL104–105 ↗#

Address of filename string executed (AT_EXECFN = 31).

def execfn : BitVec 64 := 31#64

end AuxvTag

Process Environment Inputs (AuxvConfig, ProcessInit, ProcessInputs)

def bytesOfStringL111–113 ↗#

Convert an ASCII String into List (BitVec 8) (kernel-reducible via String.toList).

def bytesOfString (s : String) : List (BitVec 8) :=
  s.toList.map fun c => BitVec.ofNat 8 c.toNat

structure AuxvConfigL115–138 ↗#

Deterministic auxiliary-vector parameters (no ASLR). Image-derived entries (AT_PHDR, AT_PHENT, AT_PHNUM, AT_PAGESZ, AT_BASE, AT_ENTRY, AT_PLATFORM, AT_RANDOM, AT_EXECFN, AT_NULL) are populated automatically by the ELF loader from ElfImage and the stack layout.

structure AuxvConfig where
  /-- 16 deterministic seed bytes placed at the `AT_RANDOM` stack pointer. -/
  randomBytes : List (BitVec 8) := List.replicate 16 0#8
  /-- `AT_HWCAP` feature bitmap (default `0x3 = HWCAP_FP | HWCAP_ASIMD` target-CPU baseline from
      `ID_AA64PFR0_EL1.FP/AdvSIMD ≠ 0xF`, matching the ISA model executing FP/SIMD instructions
      unconditionally; `arch/arm64/include/uapi/asm/hwcap.h`, `arch/arm64/kernel/cpufeature.c`). -/
  hwcap       : BitVec 64 := 0x3#64
  /-- `AT_HWCAP2` extended feature bitmap. -/
  hwcap2      : BitVec 64 := 0#64
  /-- `AT_UID`, `AT_EUID`, `AT_GID`, `AT_EGID` (default `1000`, non-setuid execution). -/
  uid         : BitVec 64 := 1000#64
  euid        : BitVec 64 := 1000#64
  gid         : BitVec 64 := 1000#64
  egid        : BitVec 64 := 1000#64
  /-- `AT_SECURE` secure-execution flag (`0` for normal non-elevated execution;
      `security/commoncap.c` `cap_bprm_creds_from_file`, `fs/binfmt_elf.c` `create_elf_tables`). -/
  secure      : BitVec 64 := 0#64
  /-- Additional `(a_type, a_val)` pairs appended before `AT_NULL`. -/
  extra       : List (BitVec 64 × BitVec 64) := []
  deriving DecidableEq, Repr, Inhabited

def defaultStackTopL140–142 ↗#

Default top of the user stack (0x0000_7fff_ffff_0000, page-aligned, below the canonical user limit and separate from fixed ET_EXEC load addresses).

def defaultStackTop : BitVec 64 := 0x00007fffffff0000#64

def defaultStackSizeL144–146 ↗#

Default user stack mapping size (8 MiB = 2048 4 KiB pages; Linux _STK_LIM in include/uapi/linux/resource.h).

def defaultStackSize : Nat := 2048 * Obj.pageSize

def defaultOracleL148–152 ↗#

Default deterministic anonymous mmap base (0x0000_6000_0000_0000), placed well above fixed ET_EXEC segments and brk heap and well below the user stack. Returning successive 64 KiB slots allows multiple anonymous mmap calls when inputs.init.oracle is not overridden.

def defaultOracle : Oracle :=
  { mmap := fun n => 0x0000600000000000#64 + BitVec.ofNat 64 (n * (16 * Obj.pageSize)) }

structure ProcessInitL154–187 ↗#

Nondeterministic kernel, hardware, and environment choices made at Linux execve(2) process-initialization time (fs/exec.c bprm_mm_init, fs/binfmt_elf.c setup_arg_pages + create_elf_tables, arch/arm64/include/asm/elf.h randomize_stack_top):

auxv: auxiliary-vector seed, credential, and CPU-feature configuration (AT_RANDOM 16-byte buffer, AT_HWCAP/AT_HWCAP2, AT_UID/AT_EUID/AT_GID/AT_EGID, AT_SECURE, and optional arch tags),
stackTop: page-aligned top of the initial user stack ([stackTop - stackSize, stackTop)),
stackSize: byte size of the initial user stack mapping (RLIMIT_STACK),
physMemAvail: available physical RAM budget in bytes (1 GiB = 2 ^ 30 by default) for dynamic writable anonymous mappings (Perm.rw) on top of initial PT_LOAD segments and the mapped user stack [stackTop - stackSize, stackTop),
oracle: nondeterministic kernel syscall and hardware store-exclusive (exclFails) oracle copied into State.oracle and State.exclFails by ElfImage.loadState.

structure ProcessInit where
  /-- Auxiliary vector configuration (`AT_RANDOM`, `AT_HWCAP`, credentials, extra tags). -/
  auxv         : AuxvConfig := {}
  /-- Page-aligned top of the initial user stack (`[stackTop - stackSize, stackTop)`). -/
  stackTop     : BitVec 64 := defaultStackTop
  /-- Size in bytes of the mapped user stack (must be a page-aligned size in `[STK_LIM, STACK_SIZE_MAX]`). -/
  stackSize    : Nat := defaultStackSize
  /-- Available physical memory budget in bytes (`2 ^ 30 = 1 GiB` by default) for dynamic
      writable (`Perm.rw`) page allocations after `PT_LOAD` segments and the user stack are
      mapped by `ElfImage.loadState`. -/
  physMemAvail : Nat := 2 ^ 30
  /-- Nondeterministic kernel and hardware oracle (`mmap`, `getrandom`, `clock_gettime`,
      and `exclFails` for spurious `STXR*`/`STLXR*`/`STXP`/`STLXP` store-exclusive failures,
      copied into `State.exclFails` by `ElfImage.loadState`). Defaults to `defaultOracle`
      (`exclFails = []`, under which store-exclusives never fail spuriously); whole-binary
      `ElfSafe`/`ElfCorrect` statements that exercise store-exclusive retry loops must quantify
      over `inputs.init.oracle` (or `inputs.init.oracle.exclFails`) rather than leaving it
      at its default. -/
  oracle       : Oracle := defaultOracle
  deriving Inhabited

structure ProcessInputsL189–214 ↗#

Complete system inputs to a Linux AArch64 ELF process, separating caller-supplied / filesystem inputs from kernel/environment initialization choices (init : ProcessInit):

User / caller-supplied inputs: command-line arguments (argv), environment variables (envp), executed filename (execfn for AT_EXECFN), standard input byte stream (stdin), and initial working-directory filesystem (files, dirs).
Nondeterministic kernel/environment init record (init : ProcessInit): auxiliary-vector parameters (init.auxv), initial stack geometry (init.stackTop, init.stackSize), available physical memory (init.physMemAvail), and syscall/hardware oracle (init.oracle, including init.oracle.exclFails).

structure ProcessInputs where
  /-- Command-line argument byte strings (`argv[0..argc-1]`, without trailing NULs). -/
  argv   : List (List (BitVec 8)) := [bytesOfString "prog"]
  /-- Environment variable byte strings (`"KEY=VALUE"`, without trailing NULs). -/
  envp   : List (List (BitVec 8)) := []
  /-- Executed filename byte string (`bprm->filename` for `AT_EXECFN`, without trailing NUL). -/
  execfn : List (BitVec 8) := []
  /-- Initial byte contents of file descriptor `0` (`stdin`). -/
  stdin  : List (BitVec 8) := []
  /-- Initial regular files `(path, bytes)` present in `State.fs.files`. -/
  files  : List (String × List (BitVec 8)) := []
  /-- Initial relative directory paths present in `State.fs`. -/
  dirs   : List String := []
  /-- Kernel/hardware/environment process-initialization choices (`auxv`, `stackTop`,
      `stackSize`, `physMemAvail`, `oracle`). -/
  init   : ProcessInit := {}
  deriving Inhabited

6 declarations not shown (lines 218–240): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Process.ProcessInputs.auxv, Arm64.Process.ProcessInputs.stackTop, Arm64.Process.ProcessInputs.stackSize, Arm64.Process.ProcessInputs.physMemAvail, Arm64.Process.ProcessInputs.oracle, Arm64.Process.ProcessInputs.ofStrings

Parsed Static ELF64 Image (ElfImage)

structure ElfImageL246–262 ↗#

A validated, statically linked AArch64 ELF64 executable image (ET_EXEC):

entry: initial program counter (e_entry),
phdrVaddr: virtual address of the ELF program header table in memory (AT_PHDR),
phent: byte size of each program header entry (e_phentsize = 56),
phnum: number of program header entries (e_phnum),
segments: page-aligned, non-overlapping PT_LOAD segments in ascending address order,
brkStart: page-aligned end of the highest PT_LOAD segment (mm->start_brk),
symbols: optional (name, vaddr) symbol table extracted from the binary.

structure ElfImage where
  entry     : BitVec 64
  phdrVaddr : BitVec 64
  phent     : Nat := 56
  phnum     : Nat
  segments  : List Snapshot.Region
  brkStart  : BitVec 64
  symbols   : List (String × BitVec 64) := []
  deriving Inhabited

Observable Process Outcome (ProcessOutcome)

structure ProcessOutcomeL266–281 ↗#

Observable outcome of a terminated process (SYS_exit, SYS_exit_group, or fatal signal ExecStatus.Signaled sig):

exitCode: exit status (code for .Exited code; BitVec.ofNat 64 (128 + sig.toNat) for .Signaled sig, matching POSIX shell $? and qemu-aarch64 exit code 134 on SIGABRT),
signal: none on normal exit/exit_group, or some sig.toNat (some 6 for SIGABRT) on fatal signal death so specifications can distinguish abort() from exit(134),
stdout: ordered sequence of bytes written to fd = 1 (OutputStream.stdout),
stderr: ordered sequence of bytes written to fd = 2 (OutputStream.stderr),
fs: final file-system state (State.fs).

structure ProcessOutcome where
  exitCode : BitVec 64
  signal   : Option Nat := none
  stdout   : List (BitVec 8)
  stderr   : List (BitVec 8)
  fs       : FsState
  deriving Inhabited

namespace ProcessOutcome

def traceStreamBytesL285–291 ↗#

Extract all bytes written to stream from an execution trace.

def traceStreamBytes (stream : OutputStream) (trace : List TraceEvent) : List (BitVec 8) :=
  trace.filterMap fun ev =>
    match ev with
    | .writeByte s b => if s == stream then some b else none
    | .userDefined _ _ => none
    | .fileChanged _ => none

def ofStateL293–299 ↗#

Project the observable ProcessOutcome from a terminated .Exited code state sf.

def ofState (code : BitVec 64) (sf : State) : ProcessOutcome :=
  { exitCode := code
    signal   := none
    stdout   := traceStreamBytes .stdout sf.trace
    stderr   := traceStreamBytes .stderr sf.trace
    fs       := sf.fs }

def ofSignalL301–308 ↗#

Project the observable ProcessOutcome from a signal-terminated .Signaled sig state sf, reporting shell / qemu-aarch64 status 128 + sig.toNat and signal := some sig.toNat.

def ofSignal (sig : BitVec 7) (sf : State) : ProcessOutcome :=
  { exitCode := BitVec.ofNat 64 (128 + sig.toNat)
    signal   := some sig.toNat
    stdout   := traceStreamBytes .stdout sf.trace
    stderr   := traceStreamBytes .stderr sf.trace
    fs       := sf.fs }

2 declarations not shown (lines 310–322): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Process.ProcessOutcome.ofTerminated?, Arm64.Process.ProcessOutcome.fileBytes?

end ProcessOutcome

end Arm64.Process