1. Today's topic

A unit test checks a specific scenario. Property-based testing checks system laws across many automatically generated scenarios.

text 
random / coverage-guided bytes
    -> semantic decoder
    -> MODEM / PHASE / CAN events
    -> production FSM
    -> invariants
    -> PASS / FAIL

The main idea: a fuzzer does not have to know the correct output for every scenario. It only needs to know properties that must never be violated.

2. Why this matters

For EC25, the fuzzer generates sequences of AT_OK, AT_ERROR, CEREG, TIMEOUT, POWER and MQTT_LOST, looking for stale-event bugs: a late OK, an old timeout or a timeout after a generation change. For the phase FSM, it generates RED/GREEN/YELLOW edges, debounce timers, stale input and ADC faults, checking that RED && GREEN does not remain quality VALID. For DMA/pool, it generates DMA_COMPLETE, CPU_ACQUIRE and CPU_RELEASE, catching double release, stale handles and ownership corruption.

3. Theory

Types of properties

Safety:

text 
RED && GREEN && quality == NORMAL never happens

Bounds:

text 
retry_count <= MAX_RETRY
queue_count <= capacity

Monotonic:

text 
transaction_id never decreases
config_generation never decreases

Consistency:

text 
mqtt == CONNECTED -> tcp == CONNECTED
state == ONLINE -> registration == REGISTERED

Idempotency:

text 
duplicate CEREG=1 does not start PDP twice

Stale-event:

text 
AT_OK tx != current_tx does not finish current transaction

Semantic decoder

It is better to feed an FSM fuzzer normalised events rather than raw bytes. For example, 4 bytes per event:

text 
byte 0: event type
byte 1: argument
byte 2: transaction relation
byte 3: generation relation

Generate interesting values: current, current-1, current+1, 0 and UINT32_MAX.

Separate parser fuzzing from FSM fuzzing

Parser fuzzing receives arbitrary bytes. FSM fuzzing receives semantic events.

Shrinking

A crash found in a sequence of 87 events should be minimised to a short sequence. LibFuzzer supports -minimize_crash=1, while a semantic shrinker can also remove events and simplify arguments.

4. Common mistakes

  1. Fuzzing the entire firmware rather than a separate core.
  2. Having no invariants.
  3. Using an incorrect property that reports false bugs.
  4. Generating only happy-path events.
  5. Generating completely random events and never reaching deep states.
  6. Not using boundary values.
  7. Not generating stale transaction/generation IDs.
  8. Using a real clock.
  9. Leaving global state between LLVMFuzzerTestOneInput() calls.
  10. Using a huge max_len from the start.
  11. Not bounding action count/internal transitions.
  12. Not using ASan/UBSan.
  13. Not minimising the reproducer.
  14. Deleting the crash input after a fix instead of keeping it in the regression corpus.

5. Practical task

Create tests/fuzz/modem/modem_fuzz.c. Events:

c 
typedef enum {
    FUZZ_EV_POWER = 0,
    FUZZ_EV_AT_OK,
    FUZZ_EV_AT_ERROR,
    FUZZ_EV_CEREG,
    FUZZ_EV_TIMER,
    FUZZ_EV_MQTT_LOST,
    FUZZ_EV_COUNT,
} fuzz_event_type_t;

Create a transaction generator:

c 
static uint32_t fuzz_transaction_id(const modem_core_t *modem, uint8_t selector)
{
    switch (selector % 5U) {
    case 0: return modem->transaction_id;
    case 1: return modem->transaction_id - 1U;
    case 2: return modem->transaction_id + 1U;
    case 3: return 0U;
    default: return UINT32_MAX;
    }
}

Check invariants:

text 
retry_count <= retry_limit
MODEM_OFF -> mqtt != CONNECTED
mqtt == CONNECTED -> modem == ONLINE
action_count <= ACTION_CAPACITY
stale AT_OK does not finish the current transaction

Build:

text 
clang -std=c17 -O1 -g -fno-omit-frame-pointer \
  -fsanitize=fuzzer,address,undefined \
  modem_core.c tests/fuzz/modem/modem_fuzz.c \
  -Icomponents/modem_core/include \
  -o build/modem_fuzz

Run:

text 
build/modem_fuzz tests/fuzz/modem/corpus -max_len=256 -max_total_time=60

6. What to try next

  • Convert .evlog from lesson 54 into a seed corpus.
  • Add a fuzz target for phase_fsm.
  • Perform differential fuzzing of the old and new FSM implementations.
  • Generate HIL scenarios from minimal fuzz cases.
Which input is most directly useful for checking that a stale AT_OK cannot complete the current transaction?

Exercise

A failure requires 87 semantic events. Describe how to turn it into a useful regression input. Also state why “transaction_id never decreases” needs an explicit epoch/wrap condition for a finite-width counter.

Self-check criteria: Retain a minimal regression input and explicitly qualify monotonicity at counter wrap.

Show the supplied answer

Minimise the sequence while retaining the failure, then keep the minimal reproducer in the regression corpus and run the same invariants. A finite-width counter can wrap from UINT32_MAX to 0, so unconditional numerical monotonicity would report a false bug; specify an epoch or a bounded no-wrap interval and test wrap handling separately.