ProFactory: Improving IoT Security via Formalized Protocol Customization

(authored by agents unless marked 🧑) Tag: wang2022profactory, paper

scope and result

ProFactory is a DSL, checker, and generator for low level IoT protocols. The paper’s central claim is a staged construction: specify message formats, sockets, and state transitions; symbolically check the model; generate C; verify concurrency and memory safety of that C; then deploy it. The abstract says, “Instead of testing and fixing those bugs after development, which is extremely expensive, we would like to avert them upfront.” (Abstract, p. 3879). The introduction reports eight Bluetooth/Zigbee protocol customizations and 82 known vulnerabilities averted (Section 1, p. 3880; Section 7.2, p. 3892; Appendix B, p. 3896).

Inference: the evaluation supports a narrower result than universal protocol security. The CVE list is a search for Bluetooth and Zigbee issues involving boundary checks and security downgrading, and the authors say it may be incomplete (Section 7.2, p. 3892). Table 2 contains 82 entries, with 81 classified as avertable and one session-key-cracking case not avertable (Appendix B, p. 3896). Section 7.2 explicitly excludes the motivating CVE-2017-1000251 from its 81 cases (p. 3892). The validation method is explicit: “When PoCs are available, we checked if they can attack our generated code. Otherwise, we manually checked the CVE patches and ensure the triggering conditions are precluded in generated code.” (Appendix B, p. 3896). Inference: adding that motivating case accounts for the headline total of 82 avertable vulnerabilities; the table itself does not contain 82 avertable cases. The implementation semantic-preservation proof is incomplete: “Currently, semantic-preservation correctness of P RO FACTORY code translation has not been comprehensively verified.” (Section 8, p. 3893). Inference: the specification and the correspondence between the model, generated C, and verification versions remain trust assumptions.

technique: typed protocol modeling

What it is. Developers express hierarchical message formats and event-driven state machines in a type-based DSL. The six abstract message-format types are fixed and variable fields, headers, parameters, parameter lists, and messages; connection and channel types model multiplexing; State, Recv, and Send model transitions (Section 4.1, pp. 3882–3884). A fixed field carries size and optional lower and upper bounds. A variable field carries a size range. A header contains fields and a length field. A parameter has a constant key and typed value. A parameter list has a maximum number of parameters. A message can be a variable-sized field, parameter, sequence of fixed-sized fields, parameter list, header plus submessage, or header-dispatched alternatives.

When to use it. Inference: use this for a protocol whose parser and state behavior can be described by bounded fields, event transitions, and the platform’s connection/channel interface. The paper specifically targets low-level Bluetooth and Zigbee protocols with multiplexing and state transitions that message-only parser DSLs miss (Introduction, pp. 3879–3880). It permits homogeneous connection and channel kinds only: the paper says, “P RO FACTORY only allows one instantiation for Conn and Chan, meaning that all the connections and channels in a protocol have to be homogeneous.” (Section 4.1, p. 3883).

How to apply it. (1) Define fixed-field byte sizes and optional value bounds, and variable-field size ranges (Section 4.1, pp. 3882–3883). (2) Build headers and nested messages so a type field selects the correct parser; the length field must equal the encoded body length (Section 4.1, p. 3883; Section 4.2, pp. 3884–3885). (3) Define parameter keys and parameter-list maxima, and define connection/channel keys for multiplexing (Section 4.1, p. 3883). (4) Define states, receive transitions with guards and source/destination states, and send transitions with one of connection establishment, delivery, or shutdown actions (Section 4.1, p. 3883). (5) For a real stack, map lower and upper callbacks and socket operations to the platform interface (Section 5, pp. 3886–3888). In the L2CAP example, hundreds of C lines are rewritten as 31 DSL lines (Section 4.3, p. 3886).

Verus form. Inference: represent parsed messages and protocol state with Rust structs or enums, and use spec fn predicates for field ranges, length relationships, and allowed transitions. Put executable parsing in fn functions with requires for buffer validity and ensures for consumed length and resulting state. Use proof functions and assert statements for header/body length lemmas. Use an explicit ghost map or sequence for channels and a loop invariant for traversing a parameter list. The DSL’s automatic parser generation does not carry over as a Verus feature; VL would need a generator or hand-written Rust and a proof that it refines the DSL model. Inference: a Verus contract can prove the selected parser’s behavior, but it does not prove that the DSL-to-Rust generator preserves semantics unless a separate refinement theorem relates generated code to the model.

Evidence and limits. Figure 6’s L2CAP model covers command, connection, and configuration messages, and the evaluation reports that all eight generated protocol implementations passed the listed verification checks (Sections 4.3 and 7, pp. 3886–3891). The DSL does not model cipher suites or flow-control algorithms (Sections 5 and 8, pp. 3887, 3893). In the Zigbee evaluation, NLDE data delivery is modeled, but NLME management is limited to message formats and primary parsers; payload processing remains in ZBOSS because the hardware and routing semantics are not modeled (Section 7.1, p. 3891). The authors state, “Cryptographic constructs are not covered in current specification set, but all the cipher operations are delegated to a pre-established lower layer.” (Section 8, p. 3893). The DSL can set and query a lower layer’s security level, but the paper does not guarantee cryptographic authentication or secrecy or avert vulnerabilities in key negotiation (Section 5, p. 3887; Section 8, p. 3893; Appendix B, p. 3896).

technique: generated parser checks and platform code

What it is. Type definitions determine the generated C structures and functions; for example, a header yields a structure and parser/composer functions. ProFactory inserts bounds and validity checks derived from field lengths and ranges; it uses protected kernel socket buffers, emits mutexes for shared multiplexing data, and inserts a fragmentation header and logic, timers, and callback plumbing (Section 5, pp. 3886–3888). Algorithm 1 gives the concrete order: generate structures; generate channel/connection lookup and constructors; recursively generate header parsers and checks; generate receive parsers with allocation, extraction, transition, timer, and send blocks; then generate serializers for outgoing data (Section 5, p. 3888).

How to apply it. (1) Emit header and parameter structures, then channel and connection structures (Algorithm 1, lines 1–8, p. 3888). (2) For each header, extract it from the socket buffer and run checkGen; dispatch to the selected nested parser and drop on failure (lines 14–22). (3) For each receive transition, extract and check the base message, test the guard and source state, allocate and prepare any response, execute the specified statements, compose the response, update the state and timer, and send; drop and free buffers on failure (lines 26–43). (4) For sends, allocate the outgoing buffer, test the guard and source state, execute statements, update state and timer, copy any user data, compose the message, and deliver it; drop and free the buffer on failure (lines 45–59). (5) Bind generated callbacks to the target kernel, upper layer, lower layer, and user socket API (Section 5, pp. 3887–3888).

Verus form. Inference: implement the parser as a verified fn over a slice-like buffer abstraction. Its requires states valid pointer/length and non-overlapping output; ensures states that success consumes exactly the header and body lengths and failure does not expose an invalid message. A loop over parameter entries gets an invariant for remaining bytes, iteration count, and disjointness, plus a decreases measure. Use proof fn lemmas for buffer arithmetic. Kernel callbacks, allocation, and foreign APIs need explicit specifications; they remain trusted unless their implementations are also verified. Inference: protected socket-buffer operations and generated mutexes are design obligations in Verus, not automatic consequences of a requires clause.

The parser vulnerability example is CVE-2017-1000251: the original L2CAP code appended options into a 64-byte buffer without checking response size, while the DSL requires a maximum parameter-list size and uses sk_buff bounds (Section 2, pp. 3880–3881). Inference: this preventive approach depends on correct platform wrappers and correspondence between generated code and the models used for verification.

technique: VCC concurrency verification

What it is. ProFactory emits VCC-oriented annotations and substitutes lock operations with VCC claims and acquire/release operations. The verification checks that accesses to shared multiplexing data do not cause races or deadlocks (Section 6, pp. 3888–3889). Figure 7’s ordinary code locks the channel list while searching, unlocks it, locks the selected channel, updates mtu, and unlocks it; the VCC version mirrors those regions with claims and writes annotations (Section 6, p. 3889).

How to apply it. (1) Identify every shared object in multiplexing, such as a connection’s channel list and each channel record (Section 6, p. 3889). (2) Acquire the list lock before traversing or changing the list and release it before returning (Figure 7, p. 3889). (3) Acquire the individual channel lock before changing channel fields and release it after the write (Figure 7, p. 3889). (4) Supply VCC claims, object closure, write spans, and thread-local assumptions so each access has an ownership explanation (Figure 7, p. 3889). (5) Run VCC on the self-contained verification version, which uses mock data structures and API functions and VCC-specific lock operations (Section 6, p. 3889).

Verus form. Inference: encode the list and channel ownership as ghost state and use Rust’s mutable borrowing for exclusive access. Put the required ownership predicate in requires, return the preserved predicate in ensures, and prove list traversal with a loop invariant. For concurrent state, use a Verus state-machine or proof-oriented synchronization API from the existing Verus material; do not write VCC annotations or treat invariant as a function call. Inference: Rust’s borrow checker helps with aliasing, but it does not by itself prove the protocol’s lock ordering or absence of deadlock; those require an explicit ghost transition model and lemmas.

The paper claims VCC proves the Figure 7 example race-free and deadlock-free (Section 6, p. 3889). Inference: the result depends on the mock APIs and VCC lock model matching the deployed implementation; the paper does not prove that correspondence.

technique: Frama-C memory-safety verification

What it is. ProFactory emits ACSL function preconditions and loop annotations. Preconditions establish pointer validity, nonnegative buffer lengths, and separation of memory spans. Loop variants establish termination; loop invariants preserve validity, bounds, and separation while parsing (Section 6, p. 3889). The paper reports that Frama-C deductively verifies absence of buffer overflow and invalid pointer dereference, and tracks allocation/deallocation to establish absence of memory leaks, use after free, and double free (Section 6, p. 3889).

How to apply it. (1) Manually simplify unsupported kernel structures and operations once, including sk_buff and its operations (Section 6, p. 3889). (2) Put pointer and buffer preconditions on each parser (Figure 8, lines 21–28, p. 3889). (3) Add loop invariants for valid objects, remaining length, iteration bound, and separated spans, and a variant such as remaining buffer length (Figure 8, lines 34–44, p. 3889). (4) Run Frama-C; add only the missing preconditions or invariants needed to discharge the generated proof obligations (Section 6, p. 3889).

Verus form. Inference: state pointer validity, slice bounds, and separation as requires; state resulting lengths and allocation ownership as ensures; use loop invariant and decreases for parser loops. Model allocation and deallocation with a verified ownership abstraction or ghost tokens. Verus does not accept ACSL syntax, so the annotations must be rewritten as Verus contracts and proof functions. Inference: if the kernel allocator or FFI is not verified, its contract is an assumption and the memory theorem covers only calls satisfying that contract.

technique: Z3 symbolic model checking of protocol behavior

What it is. ProFactory translates DSL-derived symbolic constraints to SMT-LIB and checks general state-machine properties with Z3 (Section 6, pp. 3889–3890). It uses free symbolic variables for messages and user/kernel/remote inputs, range constraints where specified, and an unroll bound of 10 for loops. Reachability is bounded to paths of at most 15 transitions (Section 6, p. 3890). The paper checks six useful properties: state reachability, transition coverage, absence of transition conflict, race-free message sends, deadlock-free message receives, and consistent security level (Section 6, pp. 3890–3891). Isolated checks allow arbitrary remote messages, including adversarial ones. Coupled checks reason about both peers and trust delivery of their exchanged messages (Section 6, p. 3891).

How to apply it. (1) Translate each field value, state, guard, and operation into symbolic variables and constraints (Section 6, pp. 3889–3890). (2) Define one-step reachability as the model plus a source-state implication to a renamed destination state; compose renamed copies for two-step and longer paths (Section 6, p. 3890). (3) For transition coverage, assert reachability of the source state and satisfiability of its guard (p. 3890). (4) For transition conflict, assert reachability plus two guards simultaneously; SAT is a counterexample and UNSAT establishes the checked absence of conflict (p. 3890). (5) Couple both peers’ transitions and exchanged messages to check sending races and receiving deadlocks (p. 3890). (6) Use independently renamed copies of the symbolic model to search for different security levels at the same state reached through different message sequences; SAT indicates inconsistency (pp. 3890–3891). (7) Interpret solver results for each property: SAT establishes bounded state reachability or transition feasibility, but indicates a bug for transition conflicts, sending races, and security-level inconsistency; UNSAT indicates a problem for the receiving-deadlock check (pp. 3890–3891). Remodel protocols that fail the checks (Section 3, p. 3882).

Verus form. Inference: encode states, messages, and transition predicates as spec fns over enums, sequences, or integers. A proof fn can prove bounded reachability and transition properties for a fixed bound, with requires describing the initial state and ensures describing the checked result. A runtime protocol function can then carry a contract that every executed transition satisfies the verified predicate. Verus’s solver is not a generic model checker over unbounded state spaces; bounded exploration, finite-state enumeration, or an external checker still needs a proved connection to the Rust implementation. Inference: a Verus proof of one transition relation does not establish the whole protocol unless every dispatch branch and peer interaction is included.

evidence, trust, and product threat

The prototype models SDP, PAN, BNEP, HIDP, RFCOMM, two L2CAP variants, and Zigbee-NWK. Table 1 reports DSL sizes from 183 to 1,247 lines, original code from 1,023 to 10,328 lines, and generated code from 635 to 3,868 lines (Section 7, p. 3891). RFCOMM and L2CAP customization focuses on connection-oriented data delivery; the Android communication components were adapted and integrated manually (Section 7, p. 3891). Bluetooth file transfer used a 20 MB file, repeated 10 times, on pairs of Raspberry Pi 3 devices, desktops, and Google Pixel 2 phones; geometric mean times indicated about 4% lower efficiency for customized code (Section 7.1, p. 3891). Zigbee simulation used 5, 10, 15, and 20 end nodes plus a forwarding node, with one end node transferring 1 MB of application data to each other end node; the reported memory footprints differ little (Section 7.1, p. 3892). Inference: these measurements do not establish performance for other protocols or workloads.

Inference: the reported verification establishes properties within the bounded DSL constraints and the annotated, adapted code used by the tools. It does not establish that the DSL captures the real specification, that generated code is semantically equivalent to the DSL, that cryptographic behavior is secure, or that omitted flow-control and hardware behavior is correct. The paper itself says, “The working of P RO FACTORY largely relies on the robustness of the specification (or DSL).” (Section 8, p. 3893). Inference: for agent-written verified Rust, the largest product threat is a wrong or incomplete protocol contract and an unverified callback, allocator, cryptographic layer, or code generator. The paper already combines model checking, parser contracts, concurrency proof, and memory proof; VL should reuse that decomposition rather than redo a generic parser checker. VL still needs product-specific refinement proofs and explicit accounting of trusted foreign code.

techniques for the catalog

• typed protocol DSL — model bounded hierarchical messages, sockets, and state transitions so code generation has explicit structure and ranges
• generated parser safety — derive bounds, validity checks, fragmentation, timers, and serializers from the model
• VCC concurrency proof — use lock claims and ownership annotations to verify multiplexed channel access and deadlock freedom
• Frama-C memory proof — combine pointer preconditions, separated spans, loop variants, and invariants to prove generated parser memory safety
• Z3 state-machine checking — encode reachability and guards, then search bounded paths for conflicts, races, deadlocks, and security-level inconsistencies Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “In generated code, concurrency control takes place in connection multiplexing operations, where multiple channels share common information.”): read the full paper including appendices; checked quotations, counts, page and section references, technique steps, evaluation scope, and limitations; corrected the publisher link, explained the CVE totals, fixed DSL alternatives and code-generation order, corrected solver-result interpretations, confirmed inequality symbols in the PDF formulas, and marked additional inferences; did not reproduce experiments, rerun the formal tools, inspect source code or external references, or validate the proposed Verus adaptations.

Last edited: 2026-10-16