{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T04:37:42Z","timestamp":1771043862313,"version":"3.50.1"},"reference-count":102,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,5]]},"DOI":"10.1109\/sp.2017.40","type":"proceedings-article","created":{"date-parts":[[2017,6,26]],"date-time":"2017-06-26T20:34:26Z","timestamp":1498509266000},"page":"503-520","source":"Crossref","is-referenced-by-count":45,"title":["SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations"],"prefix":"10.1109","author":[{"given":"Sze Yiu","family":"Chau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Endadul","family":"Hoque","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huangyi","family":"Ge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniket","family":"Kate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Nita-Rotaru","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ninghui","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","author":"gordon","year":"1993","journal-title":"Introduction to HOL A Theorem Proving Environment for Higher Order Logic"},{"key":"ref38","first-page":"3","article-title":"Model checking programs","author":"brat","year":"2000","journal-title":"IEEE International Conference on Automated Software Engineering (ASE)"},{"key":"ref33","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker blast: Applications to software engineering","volume":"9","author":"beyer","year":"2007","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503274"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"ref30","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_44"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_35"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302710"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref20","year":"0","journal-title":"CVE-2014–0092"},{"key":"ref22","first-page":"230","article-title":"On computable numbers, with an application to the entscheidungsproblem","volume":"2","author":"turing","year":"1936","journal-title":"Proceedings of the London Mathematical Society"},{"key":"ref21","year":"0","journal-title":"CVE-2014–1266"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"ref101","year":"2016","journal-title":"Vulnerability Note VU#396440-MatrixSSL contains multiple vulnerabilities"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"ref100","first-page":"646","author":"liang","year":"2014","journal-title":"A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378846"},{"key":"ref50","year":"2016","journal-title":"spark\/firmware\/communication\/lib"},{"key":"ref51","year":"2016","journal-title":"Arduino\/libraries\/ESP8266WiFi\/src\/include\/ssl h"},{"key":"ref59","year":"0","journal-title":"Package gatling (0 12cvs20120114–4) high performance web server and file server"},{"key":"ref58","year":"0","journal-title":"ipsvd-intemet protocol service daemons-installation"},{"key":"ref57","year":"0","journal-title":"how to install curl and libcurl"},{"key":"ref56","doi-asserted-by":"crossref","first-page":"20:20","DOI":"10.1145\/2602649.2602816","article-title":"Please put openssl out of its misery","volume":"12","author":"kamp","year":"2014","journal-title":"Queue"},{"key":"ref55","year":"0","journal-title":"CVE-2016–6305"},{"key":"ref54","year":"0","journal-title":"CVE-2016–7052"},{"key":"ref53","year":"0","journal-title":"CVE-2016–6303"},{"key":"ref52","year":"2017","journal-title":"MicroPython"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"ref4","first-page":"193","article-title":"Protocol state fuzzing of TLS implementations","author":"de ruiter","year":"2015","journal-title":"24th USENIX Security Symposium (USENIX Security 15)"},{"key":"ref3","article-title":"A messy state of the union: Taming the composite state machines of TLS","author":"beurdouche","year":"2015","journal-title":"IEEE Symposium on Security and Privacy"},{"key":"ref6","first-page":"223","article-title":"Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation","author":"kaloper-mer\u0161injak","year":"2015","journal-title":"24th USENIX Security Symposium (USENIX Security 15)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978411"},{"key":"ref8","first-page":"1","article-title":"FLEXTLS: A Tool for Testing TLS Implementations","author":"beurdouche","year":"2015","journal-title":"Proceedings of the 9th USENIX Conference on Offensive Technologies ser WOOT'15"},{"key":"ref49","year":"2015","journal-title":"HTTPS client is here for the Photon!"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"ref9","year":"0","journal-title":"CVE-2016–1115"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"ref45","first-page":"209","article-title":"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"OSDI"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363528"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.15"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"ref72","first-page":"363","article-title":"Apisan: Sanitizing api usages through semantic cross-checking","author":"yun","year":"2016","journal-title":"25th USENIX Security Symposium (USENIX Security 16)"},{"key":"ref71","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1109\/SP.2015.38","article-title":"Vetting ssl usage in applications with sslint","author":"he","year":"2015","journal-title":"Proc of IEEE Symposium on Security and Privacy 2015"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1145\/2248487.1950396"},{"key":"ref74","doi-asserted-by":"crossref","DOI":"10.1145\/1081706.1081750","article-title":"Cute: A concolic unit testing engine for c","author":"sen","year":"2005","journal-title":"ESEC\/FSE ACM"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2008.109"},{"key":"ref60","year":"0","journal-title":"A Python library that encapsulates wolfSSL's wolfCrypt APL"},{"key":"ref62","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"mckeeman","year":"1998","journal-title":"DIGITAL TECH-NICAL JOURNAL"},{"key":"ref61","year":"0","journal-title":"mbed TLS (PolarSSL) wrapper"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287707"},{"key":"ref64","first-page":"825","article-title":"Satisfiability modulo theories","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiabllity"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.13"},{"key":"ref67","article-title":"Prying open Pandora's box: KCI attacks against TLS","author":"hlauschek","year":"2015","journal-title":"9th USENIX Workshop on Offensive Technologies (WOOT 15)"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660338"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.17487\/rfc5280"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382204"},{"key":"ref1","article-title":"Information technology-Open Systems Interconnection-The Directory: Public-key and attribute certificate frameworks","year":"2005","journal-title":"International Telecommunication Union"},{"key":"ref95","year":"0","journal-title":"mbed TLS 2 2 0 2 1 3 1 3 15 and PolarSSL 1 2 18 released 2015"},{"key":"ref94","year":"2016","journal-title":"wolfSSL ChangeLog"},{"key":"ref93","year":"0","journal-title":"ASN 1 JavaScript decoder"},{"key":"ref92","article-title":"ASN.1 Translation","author":"gardiner","year":"2015","journal-title":"RFC 6025"},{"key":"ref91","article-title":"ASN.1 Module Definition for the LDAP and X.500 Component Matching Rules","author":"legg","year":"2013","journal-title":"RFC 3727"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"ref102","article-title":"Report on the NSF workshop on formal methods for security","volume":"abs 1608 678","author":"chong","year":"2016","journal-title":"CoRR"},{"key":"ref98","year":"2016","journal-title":"IPv6 Ready Logo Program"},{"key":"ref99","year":"2016","journal-title":"High Definition Logos"},{"key":"ref96","year":"0","journal-title":"Certificate Template Extensions Application Policy"},{"key":"ref97","author":"young","year":"2016","journal-title":"Flawed MatrixSSL Code Highlights Need for Better IoT Update Practices"},{"key":"ref10","year":"0","journal-title":"CVE-2016–5669"},{"key":"ref11","year":"0","journal-title":"CVE-2016–5672"},{"key":"ref12","year":"0","journal-title":"CVE-2016–2180"},{"key":"ref13","year":"0","journal-title":"CVE-2016–5655"},{"key":"ref14","year":"0","journal-title":"CVE-2016–3664"},{"key":"ref15","year":"0","journal-title":"CVE-2016–2113"},{"key":"ref16","year":"0","journal-title":"CVE-2016–1563"},{"key":"ref82","article-title":"Analyzing protocol implementations for interoperability","author":"pedrosa","year":"2015","journal-title":"NSDI"},{"key":"ref17","year":"0","journal-title":"CVE-2016–2562"},{"key":"ref81","first-page":"49","article-title":"Under-constrained symbolic execution: Correctness checking for real code","author":"ramos","year":"2015","journal-title":"24th USENIX Security Symposium (USENIX Security 15)"},{"key":"ref18","year":"0","journal-title":"CVE-2016–2047"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413207"},{"key":"ref19","year":"0","journal-title":"CVE-2015–5655"},{"key":"ref83","article-title":"A nice way to test openflow applications","author":"canini","year":"2012","journal-title":"NSDI"},{"key":"ref80","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1007\/978-3-642-22110-1_55","article-title":"Practical, low-effort equivalence verification of real code","author":"ramos","year":"2011","journal-title":"Proceedings of the 23rd International Conference on Computer Aided Verification ser CAV'll"},{"key":"ref89","author":"adams","year":"2002","journal-title":"Understanding PKI Concepts Standards and Deployment Considerations"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815422"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535849"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.14"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978383"}],"event":{"name":"2017 IEEE Symposium on Security and Privacy (SP)","location":"San Jose, CA, USA","start":{"date-parts":[[2017,5,22]]},"end":{"date-parts":[[2017,5,26]]}},"container-title":["2017 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx7\/7957740\/7958557\/07958595.pdf?arnumber=7958595","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,10]],"date-time":"2020-10-10T22:40:49Z","timestamp":1602369649000},"score":1,"resource":{"primary":{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/7958595\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":102,"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1109\/sp.2017.40","relation":{},"subject":[],"published":{"date-parts":[[2017,5]]}}}