HTTP/2 200 date: Wed, 04 Feb 2026 08:51:33 GMT content-type: application/json content-length: 2154 access-control-expose-headers: Link access-control-allow-headers: X-Requested-With, Accept, Accept-Encoding, Accept-Charset, Accept-Language, Accept-Ranges, Cache-Control access-control-allow-origin: * vary: Accept-Encoding content-encoding: gzip server: Jetty(9.4.40.v20210413) x-rate-limit: 5 x-rate-limit-interval: 1s x-concurrency-limit: 1 x-api-pool: public permissions-policy: interest-cohort=() {"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:05:42Z","timestamp":1746745542387,"version":"3.28.0"},"reference-count":25,"publisher":"IEEE","license":[{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,5]]},"DOI":"10.1109\/spw50608.2020.00065","type":"proceedings-article","created":{"date-parts":[[2020,12,18]],"date-time":"2020-12-18T21:38:12Z","timestamp":1608327492000},"page":"308-317","source":"Crossref","is-referenced-by-count":1,"title":["Research Report: Formally-Verified ASN.1 Protocol C-language Stack"],"prefix":"10.1109","author":[{"given":"Nika","family":"Pona","sequence":"first","affiliation":[]},{"given":"Vadim","family":"Zaliva","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"year":"0","author":"filliatre","article-title":"Extraction of programs in ocaml and haskell","key":"ref10"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1145\/3264560.3264561"},{"key":"ref12","article-title":"Quickchick: Property-based testing for coq","author":"denes","year":"0","journal-title":"Coq Workshop"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1017\/CBO9781107256552"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1007\/s10817-009-9148-3"},{"key":"ref15","article-title":"Development Team","author":"coq","year":"2017","journal-title":"The Coq Proof Assistant Reference Manual version 8 10 1"},{"year":"2013","author":"bertot","journal-title":"Interactive Theorem Proving and Program Development Coq'Art The Calculus of Inductive Constructions","key":"ref16"},{"year":"2019","author":"zaichuk","journal-title":"Formal verification of floating-point number conversion between ASN 1 BER and IEEE 754 binary encodings","key":"ref17"},{"year":"0","journal-title":"X 590 (10\/2019) Public-key and attribute certificate frameworks","key":"ref18"},{"year":"0","journal-title":"ASN 1 Encoding Rules Specification of Basic Encoding Rules (BER) Canonical Encoding Rules (CER) and Distinguished Encoding Rules (DER)","key":"ref19"},{"doi-asserted-by":"publisher","key":"ref4","DOI":"10.1145\/2560537"},{"year":"2016","author":"chirgwin","journal-title":"Guilt by ASN Compiler's bad memory bug could sting mobes cell towers telco embedded systems may inherit remote vulns","key":"ref3"},{"doi-asserted-by":"publisher","key":"ref6","DOI":"10.1145\/3133956.3134043"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1145\/1538788.1538814"},{"doi-asserted-by":"publisher","key":"ref8","DOI":"10.1145\/3229538.3229540"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1145\/3341686"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1109\/2.963441"},{"key":"ref9","first-page":"12","article-title":"Model checking large network protocol implementations","volume":"4","author":"musuvathi","year":"2004","journal-title":"NSDI"},{"year":"0","journal-title":"Abstract syntax notation one (ASN 1) specification of basic notation","key":"ref1"},{"year":"1993","author":"kaliski","journal-title":"A layman's guide to a subset of ASN 1 BER and der","key":"ref20"},{"key":"ref22","first-page":"1465","article-title":"Everparse: Verified secure zero-copy parsers for authenticated message formats","author":"ramananandro","year":"2019","journal-title":"28th USENIX Security Symposium USENIX Security 2019"},{"key":"ref21","article-title":"Monadic Parser Combinators","author":"hutton","year":"1996","journal-title":"Department of Computer Science University of Nottingham Technical Report NOTTCS-TR-96-4"},{"key":"ref24","article-title":"Challenges and possibilities for safe and secure ASN.1 encoders and decoders","author":"tullsen","year":"0","journal-title":"Fifth Workshop on Language-Theoretic Security (LangSec) Conference"},{"key":"ref23","article-title":"A formal semantics for ASN.1","author":"steckler","year":"2019","journal-title":"2019 High Confidence Software and Systems Conference"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1007\/978-3-319-96142-2_25"}],"event":{"name":"2020 IEEE Security and Privacy Workshops (SPW)","start":{"date-parts":[[2020,5,21]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2020,5,21]]}},"container-title":["2020 IEEE Security and Privacy Workshops (SPW)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9283745\/9283819\/09283873.pdf?arnumber=9283873","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T15:06:17Z","timestamp":1656601577000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9283873\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/spw50608.2020.00065","relation":{},"subject":[],"published":{"date-parts":[[2020,5]]}}}