{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:47:12Z","timestamp":1746290832026,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_63","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"909-925","source":"Crossref","is-referenced-by-count":8,"title":["Information Leakage Analysis of Complex C Code and Its application to OpenSSL"],"prefix":"10.1007","author":[{"given":"Pasquale","family":"Malacaria","sequence":"first","affiliation":[]},{"given":"Michael","family":"Tautchning","sequence":"additional","affiliation":[]},{"given":"Dino","family":"DiStefano","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"63_CR1","unstructured":"Anderson, P.: Finding heartbleed with codesonar. www.grammatech.com\/blog\/finding-heartbleed-with-codesonar"},{"key":"63_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), pp. 100\u2013114. IEEE Computer Society (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"63_CR3","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, pp. 209\u2013224. USENIX Association (2008)"},{"key":"63_CR4","unstructured":"Chou, A.: On detecting heartbleed with static analysis. security.coverity.com\/blog\/2014\/Apr\/on-detecting-heartbleed-with-static-analysis.html"},{"key":"63_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"63_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC 2003, pp. 368\u2013371. ACM (2003)","DOI":"10.1145\/775832.775928"},{"key":"63_CR7","unstructured":"Coverity. www.coverity.com"},{"key":"63_CR8","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11\u201320. IEEE Computer Society (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"63_CR9","unstructured":"Grammatech. www.grammatech.com\/codesonar"},{"key":"63_CR10","doi-asserted-by":"crossref","unstructured":"Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Twenty-Sixth Annual Computer Security Applications Conference, pp. 261\u2013269. ACM (2010)","DOI":"10.1145\/1920261.1920300"},{"key":"63_CR11","unstructured":"HP\/Fortify. saas.hp.com\/software\/fortify-on-demand"},{"key":"63_CR12","unstructured":"Klokwork. www.klokwork.com"},{"key":"63_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014)"},{"key":"63_CR14","unstructured":"Kupsch, J.A., Miller, B.P.: Why do software assurance tools have problems finding bugs like heartbleed? April 2014. continuousassurance.org\/swamp\/SWAMP-Heartbleed-White-Paper-22Apr2014-current.pdf"},{"key":"63_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"63_CR16","unstructured":"Business, R.: #339 - Neel Mehta on Heartbleed, Shellshock, October 2014. media.risky.biz\/RB339.mp.3"},{"issue":"1","key":"63_CR17","doi-asserted-by":"crossref","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(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"63_CR18","unstructured":"Schneier, B.: Heartbleed, April 2014. www.schneier.com\/blog\/archives\/2014\/04\/heartbleed.html"},{"key":"63_CR19","doi-asserted-by":"crossref","unstructured":"Seggelmann, R., Tuexen, M., Williams, M.: Transport layer security (TLS) and datagram transport layer security (DTLS) heartbeat extension. RFC 6520, RFC Editor, February 2012. www.rfc-editor.org\/rfc\/rfc6520.txt","DOI":"10.17487\/rfc6520"},{"key":"63_CR20","series-title":"Advances in Information Security","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-0-387-44599-1_13","volume-title":"Malware Detection","author":"G Smith","year":"2007","unstructured":"Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection. Advances in Information Security, vol. 27, pp. 291\u2013307. Springer, Heidelberg (2007)"},{"key":"63_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"63_CR22","unstructured":"Valgrind. valgrind.org"},{"key":"63_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Choffnes, D.R., Levin, D., Dumitras, T., Mislove, A., Schulman, A., Wilson, C.: Analysis of SSL certificate reissues and revocations in the wake of heartbleed. In: Internet Measurement Conference, pp. 489\u2013502. ACM (2014)","DOI":"10.1145\/2663716.2663758"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_63","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:10:44Z","timestamp":1568434244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}