{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:18Z","timestamp":1750221318330,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3139337.3139345","type":"proceedings-article","created":{"date-parts":[[2017,10,31]],"date-time":"2017-10-31T13:41:56Z","timestamp":1509457316000},"page":"43-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Short Paper"],"prefix":"10.1145","author":[{"given":"Samuel","family":"Gruetter","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"University of Melbourne, Melbourne, Australia"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_3"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_1_4_1","unstructured":"Andrew W. Appel and others. 2017. The Verified Software Toolchain. https:\/\/github.com\/PrincetonUniversity\/VST. (2017).  Andrew W. Appel and others. 2017. The Verified Software Toolchain. https:\/\/github.com\/PrincetonUniversity\/VST. (2017)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_6"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Mark Beaumont Jim McCarthy and Toby Murray. 2016. The Cross Domain Desktop Compositor: Using Hardware-Based Video Compositing for a MultiLevel Secure User Interface. ACM Press 533--545.  Mark Beaumont Jim McCarthy and Toby Murray. 2016. The Cross Domain Desktop Compositor: Using Hardware-Based Video Compositing for a MultiLevel Secure User Interface. ACM Press 533--545.","DOI":"10.1145\/2991079.2991087"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_6"},{"volume-title":"Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium. 207--221","author":"Beringer Lennart","key":"e_1_3_2_1_9_1"},{"key":"e_1_3_2_1_10_1","unstructured":"Daniel J. Bernstein Tanja Lange and Peter Schwabe. NaCl: Networking and Cryptography library. Available at: http:\/\/nacl.cr.yp.to\/. (????).  Daniel J. Bernstein Tanja Lange and Peter Schwabe. NaCl: Networking and Cryptography library. Available at: http:\/\/nacl.cr.yp.to\/. (????)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66402-6_16"},{"key":"e_1_3_2_1_13_1","volume-title":"State Monads and Scalable Refinement. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science)","volume":"5170","author":"Cock David","year":"2008"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"David Costanzo. 2016. Formal End-to-End Verification of Information-Flow Security for Complex Systems. Ph.D. Dissertation. Yale University. http:\/\/www.cs.yale.edu\/homes\/dsc5\/thesis.pdf.  David Costanzo. 2016. Formal End-to-End Verification of Information-Flow Security for Complex Systems. Ph.D. Dissertation. Yale University. http:\/\/www.cs.yale.edu\/homes\/dsc5\/thesis.pdf.","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_10"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66402-6_25"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSAC.2007.8"},{"key":"e_1_3_2_1_18_1","unstructured":"Samuel Gruetter. 2017. Improving the Coq proof automation tactics of the Verified Software Toolchain based on a case study on verifying a C implementation of the AES encryption algorithm. Master's thesis. \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL) Switzerland.  Samuel Gruetter. 2017. Improving the Coq proof automation tactics of the Verified Software Toolchain based on a case study on verifying a C implementation of the AES encryption algorithm. Master's thesis. \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL) Switzerland."},{"key":"e_1_3_2_1_19_1","unstructured":"Samuel Gruetter and Toby Murray. 2017. VST-Flow: Fine-Grained LowLevel Reasoning about Real-World C Code. arXiv:1709.05243 [cs] (Sept. 2017). arXiv:1709.05243  Samuel Gruetter and Toby Murray. 2017. VST-Flow: Fine-Grained LowLevel Reasoning about Real-World C Code. arXiv:1709.05243 [cs] (Sept. 2017). arXiv:1709.05243"},{"key":"e_1_3_2_1_20_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI.  Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_11"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676994"},{"key":"e_1_3_2_1_26_1","unstructured":"Donald A. MacKenzie. 2004. Mechanizing proof: computing risk and trust. MIT Press.  Donald A. MacKenzie. 2004. Mechanizing proof: computing risk and trust. MIT Press."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786558.2786561"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-0559"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Peter W. O'Hearn. 2004. Concurrency and Local Reasoning (LNCS) Vol. 3170.  Peter W. O'Hearn. 2004. Concurrency and Local Reasoning (LNCS) Vol. 3170.","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Norbert Schirmer. 2006. Verification of Sequential Imperative Programs in Isabelle-HOL. Ph.D. Dissertation. Technical University Munich.  Norbert Schirmer. 2006. Verification of Sequential Imperative Programs in Isabelle-HOL. Ph.D. Dissertation. Technical University Munich.","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"volume-title":"22nd TPHOLs (LNCS)","author":"Winwood Simon","key":"e_1_3_2_1_36_1"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0019-9"}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Dallas Texas USA","acronym":"CCS '17"},"container-title":["Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3139337.3139345","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3139337.3139345","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:49Z","timestamp":1750212829000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3139337.3139345"}},"subtitle":["Towards Information Flow Reasoning about Real-World C Code"],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":37,"alternative-id":["10.1145\/3139337.3139345","10.1145\/3139337"],"URL":"https:\/\/doi.org\/10.1145\/3139337.3139345","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}