Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE Incorrect handling of security-critical data formats, particularly in low-level languages, are the root cause of many security vulnerabilities. Provably correct parsing and serialization tools that ta...

PulseParse & EverCBOR

Uses F* and Pulse to formalize several new standards for secure data formats and attestations, including CBOR, CDDL, and COSE, producing verified libraries and compilers.

arxiv.org/abs/2505.17335

#fstarlang #pulse #everparse #rust #cbor #cddl #cose #dice #dpe