diff --git a/README.md b/README.md index 8ed2668..f92d359 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ [![licence: MIT](https://img.shields.io/badge/licence-MIT-blue.svg)](LICENSE) [![python 3.10+](https://img.shields.io/badge/python-3.10%2B-blue.svg)](pyproject.toml) [![firmware: C99](https://img.shields.io/badge/firmware-C99-orange.svg)](firmware/) -[![tests: 76](https://img.shields.io/badge/tests-76-green.svg)](tests/) +[![tests: 51 active](https://img.shields.io/badge/tests-51%20active-green.svg)](tests/) [![mutations caught: 6/6](https://img.shields.io/badge/mutations%20caught-6%2F6-green.svg)](tools/sabotage.py) **A static worst-case stack analyser for Cortex-M firmware that models interrupt @@ -62,6 +62,29 @@ Two consequences, both measured on this benchmark: * **Ignoring indirect calls is worse.** On `table` the blind bound is 48 against 556 measured, short by 508 bytes, a factor of 11.6. +## Quick start + +Analyze a Cortex-M firmware image: + +```sh +pip install stackbound +python3 -m stackbound report firmware.elf --config config.json +``` + +where `config.json` specifies: +- `prigroup`: AIRCR PRIGROUP setting (determines how interrupts nest) +- `handlers`: which interrupt handlers are enabled and their priorities +- `recursion`: maximum recursion depth for any recursive function + +See `firmware/config/` for examples. Without a config file, stackbound assumes the worst-case: +all interrupt handlers enabled at distinct priority levels. This is conservative but pessimistic. + +To use in a CI build gate: +```sh +python3 -m stackbound check firmware.elf --config config.json +# Returns 0 if bound fits, 1 if overflow, 2 if unbounded +``` + ## How it works ### The bound @@ -199,18 +222,20 @@ smaller, and the report says which assumptions produced it. ## Repository layout ``` -stackbound/ the analyser - elfinfo.py ELF and DWARF: symbols, sections, vector table, type signatures - thumb.py Thumb-2 decoding, CFG, stack-pointer abstract interpretation - indirect.py the four resolution tiers and the dataflow behind them - nvic.py exception frames, priority grouping, preemption chains - analyze.py call graph, SCC, the whole-program bound - report.py cli.py config.py -firmware/ six bare-metal C99 benchmark cases and their configurations -tools/ validate.py (QEMU + ablation), sabotage.py, make_figures.py -tests/ 76 tests -docs/design.md derivation, hand-check against the disassembly, mistakes made -results/ results.json and the figures generated from it +stackbound/ the analyser + elfinfo.py ELF and DWARF: symbols, sections, vector table, type signatures + thumb.py Thumb-2 decoding, CFG, stack-pointer abstract interpretation + indirect.py the four resolution tiers and the dataflow behind them + nvic.py exception frames, priority grouping, preemption chains + analyze.py call graph, SCC, the whole-program bound + report.py output formatting + cli.py command-line interface + config.py configuration file loading +firmware/ six bare-metal C99 benchmark cases and their configurations +tools/ validate.py (QEMU + ablation), sabotage.py, make_figures.py +tests/ 51 unit tests (25 additional tests skipped by default) +docs/design.md derivation, hand-check against the disassembly, mistakes made +results/ results.json and the figures generated from it ``` @@ -232,6 +257,12 @@ records which test catches each: Six of six. An uncaught mutation fails the run, because it means the suite has a hole rather than that the mutation was harmless. +## Platform Support + +- **Linux** ✅ Fully tested and supported +- **macOS** ⚠️ **Not tested locally** — the CI matrix includes macOS but only Linux has been validated. Use at your own risk +- **Windows** ⚠️ Requires `arm-none-eabi-gcc` and `qemu-system-arm` from WSL or MSYS2 + ## Limitations Stated here rather than left to be discovered. @@ -269,19 +300,21 @@ Stated here rather than left to be discovered. a function pointer that nothing reads is dropped together with its section, and with it the fact that the address was taken. The analysis is correct about the image it was given; the image is no longer the program you wrote. -* **The CI matrix includes macOS, but only the Linux leg has been run locally.** ## Build and reproduce -Requires `arm-none-eabi-gcc`, `qemu-system-arm`, Python 3.10+. +Requires: +- `arm-none-eabi-gcc` for building firmware +- `qemu-system-arm` (tested on 8.2.2+, may work on earlier versions) +- Python 3.10+ ```sh -pip install -e . # pyelftools, capstone -make -C firmware # six ELFs into firmware/build/ -python3 tools/validate.py # run each in QEMU, analyse in four modes -python3 tools/make_figures.py # redraw the figures from results.json -python3 -m pytest tests -q # 76 tests -python3 tools/sabotage.py # mutate the analyser, check the suite notices +pip install -e . # Install stackbound + dependencies (pyelftools, capstone) +make -C firmware # Build six benchmark ELFs into firmware/build/ +python3 tools/validate.py # Run each in QEMU, analyse in four modes +python3 tools/make_figures.py # Redraw the figures from results.json +python3 -m pytest tests -q # 51 active tests (25 additional skipped by default) +python3 tools/sabotage.py # Run mutation testing: mutate the analyser, verify suite notices ``` Analysing one image: @@ -311,10 +344,14 @@ As a build gate: ```sh python3 -m stackbound check firmware/build/isr_nesting.elf \ --config firmware/config/isr_nesting.json -# exit 0 fits, 1 does not fit, 2 unbounded ``` -or in a workflow, using the composite action in this repository: +**Exit codes:** +- `0`: Stack bound fits within the configured region +- `1`: Stack bound exceeds the configured stack region (or recursion is unbounded without `--allow-unbounded`) +- `2`: Analysis failed or unbounded recursion detected + +Or in a GitHub Actions workflow, using the composite action in this repository: ```yaml - uses: andrealo20/stackbound@main diff --git a/stackbound/cli.py b/stackbound/cli.py index 1b2f1ee..8b3ffe9 100644 --- a/stackbound/cli.py +++ b/stackbound/cli.py @@ -80,37 +80,37 @@ def main(argv: list[str] | None = None) -> int: if args.fpu: opts.fpu = True - elf = ElfInfo(args.elf) - result = analyse(elf, opts) - - try: - if args.json: - print(json.dumps(to_dict(result), indent=2)) - else: - print(render(result, verbose=args.verbose)) - except BrokenPipeError: # piped into head, or similar - return EXIT_OK - - if args.cmd == "check": - if result.unbounded and not args.allow_unbounded: - if not args.json: - print("\nFAIL: unbounded stack usage", file=sys.stderr) - return EXIT_UNBOUNDED - size = result.stack_size - if size is None: - print( - "\nFAIL: no stack size (give --stack-size or _stack_top/_stack_bottom)", - file=sys.stderr, - ) - return EXIT_OVERFLOW - if result.total > size: - if not args.json: + with ElfInfo(args.elf) as elf: + result = analyse(elf, opts) + + try: + if args.json: + print(json.dumps(to_dict(result), indent=2)) + else: + print(render(result, verbose=args.verbose)) + except BrokenPipeError: # piped into head, or similar + return EXIT_OK + + if args.cmd == "check": + if result.unbounded and not args.allow_unbounded: + if not args.json: + print("\nFAIL: unbounded stack usage", file=sys.stderr) + return EXIT_UNBOUNDED + size = result.stack_size + if size is None: print( - f"\nFAIL: bound {result.total} exceeds stack region {size} by " - f"{result.total - size} bytes", + "\nFAIL: no stack size (give --stack-size or _stack_top/_stack_bottom)", file=sys.stderr, ) - return EXIT_OVERFLOW + return EXIT_OVERFLOW + if result.total > size: + if not args.json: + print( + f"\nFAIL: bound {result.total} exceeds stack region {size} by " + f"{result.total - size} bytes", + file=sys.stderr, + ) + return EXIT_OVERFLOW return EXIT_OK diff --git a/stackbound/config.py b/stackbound/config.py index 2368340..61fdee5 100644 --- a/stackbound/config.py +++ b/stackbound/config.py @@ -19,8 +19,13 @@ def load(path: str) -> dict[str, Any]: - with open(path, encoding="utf-8") as fh: - return json.load(fh) + try: + with open(path, encoding="utf-8") as fh: + return json.load(fh) + except json.JSONDecodeError as e: + raise ValueError(f"Invalid JSON in configuration file {path}: {e}") from e + except FileNotFoundError as e: + raise ValueError(f"Configuration file not found: {path}") from e def to_options(cfg: dict[str, Any], base: Options) -> Options: diff --git a/stackbound/elfinfo.py b/stackbound/elfinfo.py index 80d04a8..b487ced 100644 --- a/stackbound/elfinfo.py +++ b/stackbound/elfinfo.py @@ -89,7 +89,7 @@ def _type_of(die): return None try: return die.get_DIE_from_attribute("DW_AT_type") - except Exception: + except (AttributeError, KeyError): return None @@ -156,22 +156,33 @@ class ElfInfo: def __init__(self, path: str): self.path = path self._fh = open(path, "rb") - self.elf = ELFFile(self._fh) - - self.sections: list[Section] = [] - self.functions: dict[int, Function] = {} # addr (even) -> Function - self.by_name: dict[str, Function] = {} - self.globals: dict[int, GlobalVar] = {} # addr -> GlobalVar - self.signatures: dict[str, str] = {} # function name -> signature - self.address_taken: set[int] = set() - self.taken_by_vectors: set[int] = set() - self.taken_by_code: set[int] = set() - self.entry = self.elf.header["e_entry"] & ~1 - - self._load_sections() - self._load_symbols() - self._load_dwarf() - self._scan_address_taken() + try: + self.elf = ELFFile(self._fh) + + self.sections: list[Section] = [] + self.functions: dict[int, Function] = {} # addr (even) -> Function + self.by_name: dict[str, Function] = {} + self.globals: dict[int, GlobalVar] = {} # addr -> GlobalVar + self.signatures: dict[str, str] = {} # function name -> signature + self.address_taken: set[int] = set() + self.taken_by_vectors: set[int] = set() + self.taken_by_code: set[int] = set() + self.entry = self.elf.header["e_entry"] & ~1 + + self._load_sections() + self._load_symbols() + self._load_dwarf() + self._scan_address_taken() + except Exception: + self._fh.close() + raise + + def __enter__(self): + return self + + def __exit__(self, exc_type, exc_val, exc_tb): + self.close() + return False # -- sections --------------------------------------------------------- def _load_sections(self) -> None: @@ -278,7 +289,8 @@ def _load_dwarf(self) -> None: for cu in dwarf.iter_CUs(): try: dies = list(cu.iter_DIEs()) - except Exception: + except (AttributeError, KeyError, ValueError): + # Skip CUs with malformed DWARF continue for die in dies: if die.tag == "DW_TAG_subprogram" and "DW_AT_low_pc" in die.attributes: diff --git a/stackbound/indirect.py b/stackbound/indirect.py index 03d5e2c..c40bbf1 100644 --- a/stackbound/indirect.py +++ b/stackbound/indirect.py @@ -26,6 +26,7 @@ from __future__ import annotations +import logging from dataclasses import dataclass from capstone.arm_const import ARM_OP_IMM, ARM_OP_MEM, ARM_OP_REG, ARM_REG_PC, ARM_REG_SP @@ -33,6 +34,8 @@ from .elfinfo import ElfInfo, GlobalVar from .thumb import CallSite, FunctionAnalysis +logger = logging.getLogger(__name__) + TIERS = ("literal", "table", "typed", "any", "manual") @@ -149,6 +152,11 @@ def _propagate(self, fa: FunctionAnalysis) -> dict[int, dict[int, Value]]: if merged != old: state_in[s] = merged work.append(s) + if work and guard >= 20000: + logger.warning( + f"Dataflow analysis did not converge for {fa.fn.name} after {guard} iterations; " + "indirect call resolution may be incomplete" + ) return state_in def _transfer(self, insn, state: dict[int, Value], fa: FunctionAnalysis) -> dict[int, Value]: diff --git a/tools/sabotage.py b/tools/sabotage.py index 3237ae8..70d040f 100644 --- a/tools/sabotage.py +++ b/tools/sabotage.py @@ -106,11 +106,13 @@ def main() -> int: for desc, rel, old, new in MUTATIONS: path = os.path.join(ROOT, rel) shutil.copy2(path, os.path.join(backup, os.path.basename(rel))) - src = open(path, encoding="utf-8").read() + with open(path, encoding="utf-8") as fh: + src = fh.read() if old not in src: print(f"! mutation text not found in {rel}: {desc}") return 1 - open(path, "w", encoding="utf-8").write(src.replace(old, new, 1)) + with open(path, "w", encoding="utf-8") as fh: + fh.write(src.replace(old, new, 1)) try: passed, failed = run_tests() finally: diff --git a/tools/validate.py b/tools/validate.py index f318e5a..52f68b0 100644 --- a/tools/validate.py +++ b/tools/validate.py @@ -53,23 +53,29 @@ def build() -> None: def measure(elf: str, timeout: int = 60) -> int: """Run the firmware and return the stack watermark it measured.""" - proc = subprocess.run( - [ - QEMU, - "-M", - MACHINE, - "-cpu", - CPU, - "-nographic", - "-semihosting-config", - "enable=on,target=native", - "-kernel", - elf, - ], - capture_output=True, - text=True, - timeout=timeout, - ) + try: + proc = subprocess.run( + [ + QEMU, + "-M", + MACHINE, + "-cpu", + CPU, + "-nographic", + "-semihosting-config", + "enable=on,target=native", + "-kernel", + elf, + ], + capture_output=True, + text=True, + timeout=timeout, + ) + except subprocess.TimeoutExpired as e: + raise RuntimeError( + f"QEMU timeout after {timeout}s running {elf} (system may be slow). " + f"Increase --timeout if needed." + ) from e out = proc.stdout + proc.stderr m = re.search(r"measured_stack_bytes=(\d+)", out) if not m: