Random.lean🔗

Entropy Syscalls

Defines the Linux AArch64 getrandom syscall number (SYS_GETRANDOM = 278), GRND_* flag constants (include/uapi/linux/random.h), and handler execGetrandom (drivers/char/random.c).

@[expose] public section

namespace Arm64

def SYS_GETRANDOML25–26 ↗#

Linux AArch64 getrandom syscall number (__NR_getrandom = 278, include/uapi/asm-generic/unistd.h:762, drivers/char/random.c:1395).

def SYS_GETRANDOM : BitVec 64 := 278#64

def GRND_NONBLOCKL28–29 ↗#

Linux getrandom flags (include/uapi/linux/random.h:47-49).

def GRND_NONBLOCK : BitVec 32 := 0x0001#32

def GRND_RANDOML30 ↗#

def GRND_RANDOM : BitVec 32 := 0x0002#32

def GRND_INSECUREL31 ↗#

def GRND_INSECURE : BitVec 32 := 0x0004#32

def GRND_KNOWN_MASKL32 ↗#

def GRND_KNOWN_MASK : BitVec 32 := GRND_NONBLOCK ||| GRND_RANDOM ||| GRND_INSECURE

def execGetrandomL34–57 ↗#

getrandom(buf, count, flags) (__NR_getrandom = 278, drivers/char/random.c:1395):

flags is unsigned int (W2): rejects bits outside GRND_KNOWN_MASK (0x7) and the mutually exclusive combination GRND_INSECURE | GRND_RANDOM (0x6) with -EINVAL.
count > MAX_RW_COUNT (0x7ffff000) returns -EINVAL without writing memory or advancing oracleIdx (Linux clamps count to MAX_RW_COUNT for a short read).
Assumes an initialized kernel CRNG, so GRND_NONBLOCK never returns -EAGAIN and valid requests fill count bytes from s.oracle.getrandom s.oracleIdx.
Checks flags before checking s.mem.canWrite buf count.toNat (copy_to_user).

def execGetrandom (s : State) : State :=
  let buf := s.readReg64 Reg.x0
  let count := s.readReg64 Reg.x1
  let flags := s.readReg32 Reg.x2
  if (flags &&& ~~~GRND_KNOWN_MASK) != 0#32 ||
      (flags &&& (GRND_RANDOM ||| GRND_INSECURE)) == (GRND_RANDOM ||| GRND_INSECURE) ||
      count.toNat > MAX_RW_COUNT then
    (s.writeReg64 Reg.x0 (-EINVAL)).advancePC
  else if !s.mem.canWrite buf count.toNat then
    (s.writeReg64 Reg.x0 EFAULT_RET).advancePC
  else
    let bytes := (List.range count.toNat).map (s.oracle.getrandom s.oracleIdx)
    (((s.setMem (s.mem.writeBytes buf bytes)).nextOracle).writeReg64 Reg.x0 count).advancePC

end Arm64