Internet of Things (IoT) devices heavily rely on lightweight communication protocols such as MQTT, CoAP, and 6LoWPAN. To minimize memory footprint and computational overhead, these protocols are often implemented using custom C/C++ code, making them highly susceptible to memory corruption vulnerabilities including buffer overflows and integer underflows. Traditional automated testing techniques, such as coverage-guided fuzzing and standard symbolic execution, struggle to effectively explore the deep state spaces of these protocols due to the complex, stateful nature of network handshakes and the path explosion problem. In this paper, we propose ProtoSym, a novel State-Aware Hybrid Concrete-Symbolic Engine designed specifically for IoT protocol vulnerability discovery. Our approach synergistically combines directed concrete execution to navigate complex network state machines with selective symbolic execution to rigorously solve constraints within packet payloads, effectively finding deep-seated security flaws in IoT gateway firmware. We introduce a formal theoretical framework that models protocol states and transitions, enabling precise constraint formulation, and present a directed path exploration strategy that mitigates path explosion while maximizing state coverage. Experimental evaluation on widely-used IoT protocol implementations demonstrates that ProtoSym achieves up to 46.7% higher statespace coverage and discovers $3.7 \times$ more unique vulnerabilities compared to state-of-the-art baselines.
Gautham Koorma, Isaac Pflaum, Radostin Pachamanov et al.· International Conference on...· 0 citations
High-impact generative AI makes catastrophic misuse a lifecycle-control problem, not merely a prompt-filtering problem. SAGE is a safety-first, authorization-separated architecture in which credible catastrophic-enablement risk constrains admissibility before utility, latency, or commercial objectives are considered. It combines signed release manifests, diverse detectors, robust risk envelopes, least-risk defaults, output checking, three-valued monitoring, protected audit chains, containment, and rollback. Formal results establish safety priority, conservative detector bounds, monotone release gating, tamper-evident records, and an authorization cut; two PRISM abstractions verify authorization separation and lifecycle invariants under explicit assumptions. A frozen, vendor-symmetric study sent 84 cases to each of four GPT, four Claude, and two Gemini snapshots: 840 calls yielded 794 target responses, 46 provider errors, and 449 successful judgments covering 375 responses. Eight snapshots had complete judged domain coverage. Harmful-compliance estimates were low; variation arose mainly from benign utility and safe redirection. Seven multiplicity-adjusted contrasts involving Claude, Gemini, or GPT-5 snapshots and the GPT-5 mini and GPT-5 nano snapshots were supported, while no tested contrast between the Claude or Gemini snapshots and GPT-5 or GPT-5.5 survived correction. The observed harmful-compliance range is a conservative, protocol-bound view from one generation per prompt with no tools, retrieval, history, or human adjudication; it is not an upper bound on operational assistance. A preregistered extension specifies how to test a wider best-worst gap using a locked split, repeated sampling, multi-turn and sandboxed-tool conditions, and domain-expert scoring.
