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.

Known Issues

Auto-add of SYSTEM fails when the module has no IMPORT clause at all. The "If SYSTEM is not in the module's IMPORT list, the tool adds it automatically" behaviour described above works only when an IMPORT line already exists. If the source module has no IMPORT clause, the tool inserts the epilogue (using SYSTEM.LDREG/EMIT/EMITH) but does not add an IMPORT SYSTEM; line, and the module then fails to compile. Workaround: add IMPORT SYSTEM; to the module by hand. To be fixed in a future version.

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