sec-epilogue

Insert Secure return epilogues into exported procedures

Name

sec-epilogue – insert Secure epilogues into exported procedures

Synopsis

sec-epilogue Module.mod [Module2.mod …] [--no-clear] [--dry-run]

Description

sec-epilogue reads an Oberon .mod file and its corresponding .lst listing, analyses the stack frame of each exported procedure, and inserts a BXNS return epilogue before the END ProcName; statement.

The tool generates SYSTEM.EMIT, SYSTEM.EMITH, and SYSTEM.LDREG calls directly (hex constants, no module references). By default, full register sanitisation is included (adversarial mode). With --no-clear, only the stack deallocation and BXNS return sequence is generated (cooperative mode).

The .lst file is expected alongside the .mod file (same directory, same base name). If not found, a warning is issued and the module is skipped.

The tool modifies the .mod file in place using (* +sec-epilogue *) and (* -sec-epilogue *) markers. Re-running replaces the generated block. If SYSTEM is not in the module's IMPORT list, the tool adds it automatically.

Arguments

Module.mod: One or more .mod files. The corresponding .lst file must exist in the same directory with the same base name.

Options

--no-clear: Skip register sanitisation. Only generate stack deallocation + POP.W {LR} + BXNS LR. Use when Secure and Non-secure images trust each other (cooperative model).
--dry-run, -n: Show what would be generated without writing. Prints per-procedure analysis (push count, sub bytes, deallocation, etc.).

Workflow

The module is compiled twice:

1. compile Module.mod        -> Module.lst (first compilation)
2. sec-epilogue Module.mod   -> inserts epilogues into Module.mod
3. compile Module.mod        -> Module.arm (second compilation)
...
- link
- gen-secure ...             -> NSC.bin, NS_*.mod

The inserted SYSTEM.EMIT/EMITH/LDREG calls do not affect the stack frame, so the prologue is identical between the two compilations.

Sanitisation Modes

Default (adversarial)

Full register clearing before BXNS return:

GPR: clear R0 – R11 (R1 – R11 for function procedures that return a value in R0). R12 is excluded – not used by the compiler; if used via inline assembly, clearing is the programmer's responsibility.
APSR: clear condition flags via MSR APSR_nzcvq, R1.
FPU (if FPU instructions detected in the procedure): clear D0 – D15 (= S0 – S31) via VMOV Dd, R1, R1, then clear FPSCR via VMSR FPSCR, R1.
Stack deallocation: ADD SP, #N (narrow or wide encoding as needed).
Return: POP.W {LR} + BXNS LR.

Cooperative (`--no-clear`)

No register clearing:

Stack deallocation: ADD SP, #N.
Return: POP.W {LR} + BXNS LR.

Stack Frame Analysis

The tool reads the .lst to determine the exact stack frame for each exported procedure:

Push count: from the push/push.w instruction at the procedure entry. Handles narrow PUSH, wide STMDB, and wide STR (single-register push.w).
Sub bytes: from sub sp,#N or sub.w sp,sp,#N immediately after the push. Also handles register-based sub.w sp,sp,rN with a preceding movw rN,#imm (compiler pattern for large locals).
Deallocation: (push_count - 1) * 4 + sub_bytes. LR is popped separately by POP.W {LR}.

For large deallocation values (> 508 bytes), the tool generates wide ADD.W SP, SP, #imm (Thumb2 modified immediate) split into multiple instructions if needed.

Generated Code

Example for a procedure with push { r0, lr } + sub sp, #12 (dealloc = 4 + 12 = 16):

(* +sec-epilogue *)
  SYSTEM.LDREG(0, 0); (* clear r0 *)
  SYSTEM.LDREG(1, 0); (* clear r1 *)
  ...
  SYSTEM.LDREG(11, 0); (* clear r11 *)
  SYSTEM.EMIT(0F3818800H); (* msr APSR_nzcvq, r1 *)
  SYSTEM.EMITH(0B004H); (* add sp, #16 *)
  SYSTEM.EMIT(0E8BD4000H); (* pop.w {lr} *)
  SYSTEM.EMITH(04774H) (* bxns lr *)
(* -sec-epilogue *)
END ProcName;

Procedures Not Transformed

Non-exported procedures
Exception handlers
The module ..init block

Limitations

Double compilation: the .lst from the first compilation is needed. If the source changes, both compilations must be repeated.
Nested procedures: not supported.

Examples

Single module

python sec-epilogue.py S0.mod

Multiple modules

python sec-epilogue.py S0.mod S1.mod S2.mod

Cooperative mode (no sanitisation)

python sec-epilogue.py S0.mod --no-clear

Dry run

python sec-epilogue.py S0.mod --dry-run

Output:

sec-epilogue: would update S0.mod
  ToggleLED: push=2 sub=4100 dealloc=4104 gpr=r2 fpu=yes func=no
  SetBits: push=3 sub=12 dealloc=20 gpr=r1 fpu=no func=no