Hello,
My name is Tahina Ramananandro and I am a research engineer at Microsoft Research RiSE [0]. With a few colleagues at RiSE, we have recently been studying the CBOR and CDDL specifications and have produced a formal model of them, backed by formally verified executable code: we now have formally verified C and Rust implementations of CBOR and COSE signing, as well as a formally verified parser and serializer generator from CDDL data descriptions, all proven correct for memory safety, arithmetic safety, functional correctness, non-ambiguity, and (for the deterministic subset of CBOR) non-malleability. The runtime performance of our implementation is in the ballpark of existing unverified implementations such as qcbor and tinycbor; we validate Deterministic CBOR in constant stack space. Further details in the paper that we posted on arXiv [1], which has just been accepted to ACM CCS 2025. The code and proofs [2] and a pre-built Docker image [3] are all available on GitHub. If you are interested, here is a list of events at IETF 123 relevant to our verified implementation: * On Saturday 19th and Sunday 20th, you are welcome to join a hackathon that I will host to demo and benchmark our verified implementation, and to assess its applicability to protocols based on CBOR and CDDL, such as EDHOC or OSCORE. No prior formal methods background needed. More details at https://wiki.ietf.org/en/meeting/123/hackathon#benchmarking-evercbor-and-evercddl-formally-verified-parsers-and-serializers-for-cbor-and-cddl * On Tuesday 22nd, 17:00-18:30 CEST in the Segovia room, Carsten Bormann will host a side meeting where I will present our verified implementation. More details at https://trello.com/c/zW1S6z84 * On Thursday 24th at the UFMRG meeting, I will give a broader 30-minute talk on EverParse, our research project on formally verified parsing for binary data formats. More details at https://project-everest.github.io/everparse/ * On Friday 25th at the CBOR WG meeting, I will give a 15-minute talk on our verified implementation, including a report on the hackathon and the side meeting. Thank you, and see you in Madrid, -- Tahina Ramananandro Principal Research SDE RiSE - Research in Software Engineering Microsoft Research 1 Microsoft Way, Building 99, Office 2240 Redmond, WA 98052, USA Email: [email protected]<mailto:[email protected]> Web page: https://www.microsoft.com/en-us/research/people/taramana/ References: [0] MSR RiSE: Research in Software Engineering. https://www.microsoft.com/en-us/research/group/research-software-engineering-rise/ [1] Tahina Ramananandro, Gabriel Ebner, Guido MartÃnez and Nikhil Swamy. Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL and COSE. May 2025. https://arxiv.org/abs/2505.17335 [2] GitHub code and proofs for EverParse. https://github.com/project-everest/everparse [3] Pre-built Docker images for EverCBOR. https://github.com/project-everest/everparse/pkgs/container/evercbor
_______________________________________________ Ace mailing list -- [email protected] To unsubscribe send an email to [email protected]
