{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:48Z","timestamp":1775873568653,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319664019","type":"print"},{"value":"9783319664026","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66402-6_16","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T13:44:11Z","timestamp":1502459051000},"page":"260-277","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Verifying Constant-Time Implementations by Abstract Interpretation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,12]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Acii\u00e7mez, O., Ko\u00e7, \u00c7.K., Seifert, J.-P.: On the power of simple branch prediction analysis. In: ACM Symposium on Information, Computer and Communications Security (2007)","DOI":"10.1145\/1229285.1266999"},{"key":"16_CR2","unstructured":"Almeida, J.B., et al.: Verifying constant-time implementations. In: 25th USENIX Security Symposium, USENIX Security 16 (2016)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Andrysco, M., et al.: On subnormal floating point and abnormal timing. In: Proceedings of the 2015 IEEE Symposium on Security and Privacy (2015)","DOI":"10.1109\/SP.2015.44"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., et al.: Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of FMCO 2005 (2005)","DOI":"10.1007\/11804192_17"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., et al.: System-level non-interference for constant-time cryptography. In: Conference on Computer and Communications Security (CCS) (2014)","DOI":"10.1145\/2660267.2660283"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J.: Curve25519: new Diffie-Hellman speed records. In: Public Key Cryptography - PKC 2006: 9th International Conference on Theory and Practice in Public-Key Cryptography (2006)","DOI":"10.1007\/11745853_14"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J., Lange, T., Schwabe, P.: The security impact of a new cryptographic library. In: International Conference on Cryptology and Information Security in Latin America (2012)","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI (2003)","DOI":"10.1145\/781131.781153"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Blazy, S., Laporte, V., Pichardie, D.: An abstract memory functor for verified C static analyzers. In: International Conference on Functional Programming (ICFP 2016) (2016)","DOI":"10.1145\/2951913.2951937"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Bos, J.W., et al.: Post-quantum key exchange for the TLS protocol from the ring learning with errors problem. In: IEEE Symposium on Security and Privacy, SP 2015 (2015)","DOI":"10.1109\/SP.2015.40"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-540-45146-4_34","volume-title":"Advances in Cryptology - CRYPTO 2003","author":"B Canvel","year":"2003","unstructured":"Canvel, B., Hiltgen, A., Vaudenay, S., Vuagnoux, M.: Password interception in a SSL\/TLS channel. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 583\u2013599. Springer, Heidelberg (2003). doi:10.1007\/978-3-540-45146-4_34"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages, POPL 1977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR13","unstructured":"ctgrind. https:\/\/github.com\/agl\/ctgrind"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Proceedings of 2nd International Conference on Security in Pervasive Computing (2005)","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19, 236\u2013243 (1976)","journal-title":"Commun. ACM"},{"key":"16_CR16","unstructured":"donna. https:\/\/code.google.com\/archive\/p\/curve25519-donna"},{"key":"16_CR17","unstructured":"Doychev, G., et al.: CacheAudit: a tool for the static analysis of cache side channels. In: USENIX Conference on Security (2013)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Al Fardan, N.J., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: Symposium on Security and Privacy (SP 2013) (2013)","DOI":"10.1109\/SP.2013.42"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Feret, J.: Static analysis of digital filters. In: European Symposium on Programming (ESOP 2004) (2004)","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Sec. 8, 399\u2013422 (2009)","journal-title":"Int. J. Inf. Sec."},{"key":"16_CR21","unstructured":"Hedin, D., Sabelfeld, A.: A perspective on information-flow control. In: Software Safety and Security - Tools for Analysis and Verification (2012)"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Jourdan, J.-H., et al.: A formally-verified C static analyzer. In: Symposium on Principles of Programming Languages, POPL 2015 (2015)","DOI":"10.1145\/2676726.2676966"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Kocher, P.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Advances in Cryptology - CRYPTO 1996 (1996)","DOI":"10.1007\/3-540-68697-5_9"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Lattner, C., Lenharth, A., Adve, V.S.: Making contextsensitive points-to analysis with heap cloning practical for the real world. In: Conference on Programming Language Design and Implementation, PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250766"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52, 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"16_CR26","unstructured":"mbed TLS (formerly known as PolarSSL). https:\/\/tls.mbed.org\/"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006) (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Higher-Order and Symbolic Computation (2006)","DOI":"10.1007\/s10990-006-8609-1"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: Symposium on Principles of Programming Languages, POPL 1999 (1999)","DOI":"10.1145\/292540.292561"},{"key":"16_CR30","unstructured":"Open Quantum Safe. https:\/\/openquantumsafe.org\/"},{"key":"16_CR31","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25, 117\u2013158 (2003)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Reparaz, O., Balasch, J., Verbauwhede, I.: Dude, is my code constant time. In: Proceedings of DATE 2017 (2017)","DOI":"10.23919\/DATE.2017.7927267"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Rodrigues, B., Quint\u00e3o Pereira, F.M., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In: Compiler Construction (2016)","DOI":"10.1145\/2892208.2892230"},{"key":"16_CR34","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21, 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"16_CR35","unstructured":"TIS-CT. http:\/\/trust-in-soft.com\/tis-ct\/"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Wheeler, D.J., Needham, R.M.: TEA, a tiny encryption algorithm. In: Fast Software Encryption: Second International Workshop Leuven (1995)","DOI":"10.1007\/3-540-60590-8_29"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Zhao, J.: et al.: Formalizing the LLVM intermediate representation for verified program transformation. In: Symposium on Principles of Programming Languages, POPL 2012 (2012)","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2017"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66402-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T00:05:40Z","timestamp":1660521940000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66402-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319664019","9783319664026"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66402-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 August 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESORICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Research in Computer Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 September 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esorics2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/deic.uab.cat\/conferences\/dpm\/dpm2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}