Reported 32-bit ss_flags word for sas at stack pointer sp (sas_ss_flags(sp) | (current->sas_ss_flags & SS_FLAG_BITS) in include/linux/sched/signal.h:602-608 and kernel/signal.c:4468-4469).

rt_sigprocmask(how, set, oldset, sigsetsize) (__NR_rt_sigprocmask = 135, kernel/signal.c:3247 SYSCALL_DEFINE4(rt_sigprocmask)): validates sigsetsize == 8 (sizeof(sigset_t) on 64-bit Linux), user-memory readability and non-wrapping 8-byte range of set (when non-null), how ∈ {SIG_BLOCK(0), SIG_UNBLOCK(1), SIG_SETMASK(2)} when set ≠ 0, and writability and non-wrapping 8-byte range of oldset (8 bytes when non-null).

• [INTENTIONAL_SCOPE]: Non-zero blocked signal masks are out of scope. Because a process starts with an empty blocked mask (0), set == 0, how == SIG_UNBLOCK(1), and SIG_BLOCK(0) / SIG_SETMASK(2) with (read64 set &&& ~~~SIG_UNBLOCKABLE_MASK) == 0 (SIGKILL / SIGSTOP stripped per sigdelsetmask in kernel/signal.c:3262) all preserve an empty blocked mask (oldset receives 8 zero bytes when non-null), whereas SIG_BLOCK or SIG_SETMASK with any blockable signal bit set fails closed with .Exception.

• [OVERPINNED_BEHAVIOR]: Validates sigsetsize -> copy_from_user(set) -> how / empty-mask scope check -> copy_to_user(oldset), matching kernel/signal.c:3254-3281.

sigaltstack(uss, uoss) (__NR_sigaltstack = 132, SYSCALL_DEFINE2(sigaltstack) and do_sigaltstack in kernel/signal.c:4458-4527): models queries and updates of the per-thread 24-byte stack_t alternate signal stack (ss_sp : u64 at +0, 32-bit ss_flags at +8 ignoring 4-byte caller padding at +12, ss_size : u64 at +16):

• non-null uss that wraps modulo 2 ^ 64 or is not 24-byte readable returns -EFAULT (copy_from_user(&new, uss, sizeof(stack_t)) before state mutation);

• when uss ≠ 0 and s.sigAltStack.onSigStack s.sp (sp ∈ (sas.sp, sas.sp + sas.size] without SS_AUTODISARM), returns -EPERM;

• when uss ≠ 0 and (ss_flags &&& ~~~SS_AUTODISARM) ∉ {0, SS_ONSTACK, SS_DISABLE}, returns -EINVAL;

• when uss ≠ 0 and (ss_flags &&& ~~~SS_AUTODISARM) == SS_DISABLE, records { sp := 0, size := 0, ssFlags := ss_flags } without checking ss_size (kernel/signal.c:4496-4499); otherwise records { sp := ss_sp, size := ss_size, ssFlags := ss_flags } after requiring ss_size ≥ MINSIGSTKSZ (5120, returning -ENOMEM if smaller) unless the recorded (sas_ss_sp, sas_ss_size, sas_ss_flags) already equals (ss_sp, ss_size, ss_flags): that unchanged-settings early return (kernel/signal.c:4486-4493, after the -EPERM/-EINVAL checks and before SS_DISABLE normalization and the MINSIGSTKSZ check) leaves the state unchanged, which equals the store below (every reachable recorded SS_DISABLE-mode setting already has sp = size = 0);

• when uoss ≠ 0, writes the previous 24-byte zero-padded stack_t snapshot (oldBytes, captured before updating s.sigAltStack) to uoss (returning -EFAULT if uoss wraps modulo 2 ^ 64 or is not 24-byte writable, matching copy_to_user(uoss, &old, sizeof(stack_t)) after do_sigaltstack in kernel/signal.c:4521-4525);

• [OVERPINNED_BEHAVIOR]: checks copy_from_user(uss) -> do_sigaltstack -> copy_to_user(uoss), matching kernel/signal.c:4519-4526.

rt_sigaction(signum, act, oldact, sigsetsize) (__NR_rt_sigaction = 134, SYSCALL_DEFINE4(rt_sigaction) and do_sigaction in kernel/signal.c:4551): models per-signal SIG_DFL (0) and SIG_IGN (1) disposition queries and updates across the 64 Linux signals (1 ≤ signum ≤ 64, _NSIG = 64), plus recording user-space handlers for the synchronous hardware fault signals SIGBUS (7) and SIGSEGV (11), in State.sigActions without asynchronous signal delivery:

• sigsetsize != 8 (sizeof(sigset_t)) returns -EINVAL;

• non-null act that wraps modulo 2 ^ 64 or is not 32-byte readable returns -EFAULT (copy_from_user);

• signum ≤ 0 or signum > 64 returns -EINVAL (!valid_signal(sig));

• non-null act with signum == SIGKILL (9) or signum == SIGSTOP (19) returns -EINVAL (sig_kernel_only(sig));

• [INTENTIONAL_SCOPE]: non-null act whose sa_handler is neither SIG_DFL (0) nor SIG_IGN (1) is permitted only when signum == SIGSEGV (11) or signum == SIGBUS (7) (recording the disposition in State.sigActions); all other signals fail closed with .Exception "unmodeled rt_sigaction". Hardware faults in Arm64/Trusted/ISA/Eval.lean always raise .Exception directly (never .Signaled or invoking user handlers), and execTkill / execTgkill on SIGSEGV / SIGBUS or non-SIG_DFL/SIG_IGN SIGABRT likewise raise .Exception;

• when act ≠ 0, records { handler, flags &&& UAPI_SA_FLAGS, restorer, mask &&& ~~~SIG_UNBLOCKABLE_MASK } in State.sigActions signum (sa_flags &= UAPI_SA_FLAGS and sigdelsetmask in do_sigaction); recorded flags are thus already masked, so oldact matches Linux's oact->sa.sa_flags &= UAPI_SA_FLAGS;

• when oldact ≠ 0, writes the previous 32-byte k_sigaction to oldact (returning -EFAULT if oldact wraps modulo 2 ^ 64 or is not 32-byte writable, matching copy_to_user after do_sigaction);

• [OVERPINNED_BEHAVIOR]: checks sigsetsize -> copy_from_user(act) -> do_sigaction(signum) -> copy_to_user(oldact), matching kernel/signal.c:4559-4573.

tkill(tid, sig) (__NR_tkill = 130, do_tkill in kernel/signal.c:4038):

• if tid ≤ 0, sig < 0, or sig > 64 (_NSIG), returns -EINVAL;

• [INTENTIONAL_SCOPE]: if tid == 1 (SIM_TID) and sig == SIGABRT (6):

  • when SIGABRT's disposition is SIG_DFL (0), terminates the process with fatal signal status .Signaled 6#7 (shell / qemu-aarch64 exit code 128 + 6 = 134);

  • when SIGABRT's disposition is SIG_IGN (1), drops the ignored signal (sig_ignored in kernel/signal.c) and returns 0;

  • otherwise fails closed with .Exception "unmodeled tkill";

• any other (tid, sig) pair fails closed with .Exception "unmodeled tkill".

tgkill(tgid, tid, sig) (__NR_tgkill = 131, do_tkill in kernel/signal.c:4024):

• if tid ≤ 0, tgid ≤ 0, sig < 0, or sig > 64 (_NSIG), returns -EINVAL;

• [INTENTIONAL_SCOPE]: if tgid == 1, tid == 1 (SIM_TID), and sig == SIGABRT (6):

  • when SIGABRT's disposition is SIG_DFL (0), terminates the process with fatal signal status .Signaled 6#7 (shell / qemu-aarch64 exit code 128 + 6 = 134);

  • when SIGABRT's disposition is SIG_IGN (1), drops the ignored signal (sig_ignored in kernel/signal.c) and returns 0;

  • otherwise fails closed with .Exception "unmodeled tgkill";

• any other (tgid, tid, sig) triple fails closed with .Exception "unmodeled tgkill".