{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:48:14Z","timestamp":1759092494588,"version":"3.37.3"},"reference-count":71,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T00:00:00Z","timestamp":1505520000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T00:00:00Z","timestamp":1505520000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-12-2-0012","HR0011-16-C-0059"],"award-info":[{"award-number":["HR0011-12-2-0012","HR0011-16-C-0059"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["CCF-0904371","CNS-1228782"],"award-info":[{"award-number":["CCF-0904371","CNS-1228782"]}]},{"name":"National Science Foundation","award":["CNS-1228620","CNS-1528108"],"award-info":[{"award-number":["CNS-1228620","CNS-1528108"]}]},{"name":"National Science Foundation","award":["1526211"],"award-info":[{"award-number":["1526211"]}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8650-10-C-7088","FA8750-14-2-0270"],"award-info":[{"award-number":["FA8650-10-C-7088","FA8750-14-2-0270"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-15-C-0082","FA8650-15-C-7562"],"award-info":[{"award-number":["FA8750-15-C-0082","FA8650-15-C-7562"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8650-15-C-7562"],"award-info":[{"award-number":["FA8650-15-C-7562"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s10703-017-0296-5","type":"journal-article","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T10:53:07Z","timestamp":1505559187000},"page":"362-394","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Program synthesis for interactive-security systems"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7667-1287","authenticated-orcid":false,"given":"William R.","family":"Harris","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas W.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,16]]},"reference":[{"key":"296_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: CAV","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"296_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin M M K, Raghothaman M, Seshia S A, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"2","key":"296_CR3","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.tcs.2005.11.017","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur R, La Torre S, Madhusudan P (2006) Modular strategies for recursive game graphs. Theor Comput Sci 354(2):230\u2013249","journal-title":"Theor Comput Sci"},{"key":"296_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Madhusudan P (2004) Visibly pushdown languages. In: STOC","DOI":"10.1145\/1007352.1007390"},{"key":"296_CR5","unstructured":"ARM (2016) Products. \n                    https:\/\/www.arm.com\/products\/security-on-arm\/trustzone\n                    \n                  . Accessed 9 Sept 2016"},{"key":"296_CR6","doi-asserted-by":"crossref","unstructured":"Barthe G, Fournet C, Gr\u00e9goire B, Strub P-Y, Swamy N, B\u00e9guelin SZ (2014) Probabilistic relational verification for cryptographic implementations. In: POPL","DOI":"10.1145\/2535838.2535847"},{"key":"296_CR7","unstructured":"Bittau A, Marchenko P, Handley M, Karp B (2008) Wedge: splitting applications into reduced-privilege compartments. In: NSDI"},{"key":"296_CR8","unstructured":"Brumley D, Song D X (2004) Privtrans: automatically partitioning programs for privilege separation. In: USENIX security symposium"},{"key":"296_CR9","unstructured":"C. E. Board. CVE-2007-4476. \n                    http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2007-4476\n                    \n                  , Aug 2007"},{"key":"296_CR10","unstructured":"C. E. Board. GNU Tar and GNU Cpio rmt_read__() function buffer overflow. \n                    http:\/\/xforce.iss.net\/xforce\/xfdb\/56803\n                    \n                  , Mar 2010"},{"issue":"11","key":"296_CR11","first-page":"1471","volume":"5","author":"A Cheung","year":"2012","unstructured":"Cheung A, Arden O, Madden S, Myers AC (2012) Automatic partitioning of database applications. PVLDB 5(11):1471\u20131482","journal-title":"PVLDB"},{"key":"296_CR12","doi-asserted-by":"crossref","unstructured":"Chong S, Liu J, Myers A C, Qi X, Vikram K, Zheng L, Zheng X (2007) Secure web application via automatic partitioning. In: SOSP","DOI":"10.1145\/1294261.1294265"},{"issue":"6","key":"296_CR13","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157\u20131210","journal-title":"J Comput Secur"},{"key":"296_CR14","unstructured":"Costan V, Lebedev I, Devadas S (2015) Sanctum: minimal hardware extensions for strong software isolation. Cryptology ePrint Archive, Report 2015\/564. \n                    http:\/\/eprint.iacr.org\/"},{"key":"296_CR15","unstructured":"CVE-2004-1488. \n                    http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CAN-2004-1488\n                    \n                  , Feb 2005"},{"key":"296_CR16","unstructured":"CVE-2007-3798. \n                    http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2007-3798\n                    \n                  , July 2007"},{"key":"296_CR17","unstructured":"CVE-2010-0405. \n                    http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2010-0405\n                    \n                  , Apr 2010"},{"issue":"5","key":"296_CR18","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning DE (1976) A lattice model of secure information flow. Commun ACM 19(5):236\u2013243","journal-title":"Commun ACM"},{"key":"296_CR19","doi-asserted-by":"crossref","unstructured":"Efstathopoulos P, Kohler E (2008) Manageable fine-grained information flow. In: EuroSys","DOI":"10.1145\/1352592.1352624"},{"key":"296_CR20","doi-asserted-by":"crossref","unstructured":"Efstathopoulos P, Krohn M N, Vandebogart S, Frey C, Ziegler D, Kohler E, Mazi\u00e8res D, Kaashoek MF, Morris R (2005) Labels and event processes in the Asbestos operating system. In: SOSP","DOI":"10.1145\/1095810.1095813"},{"key":"296_CR21","unstructured":"Erlingsson \u00da, Schneider FB (2000) IRM enforcement of Java stack inspection. In: SSP"},{"key":"296_CR22","unstructured":"FreeBSD 9.0-RELEASE announcement. \n                    http:\/\/www.freebsd.org\/releases\/9.0R\/announce.html\n                    \n                  , Jan 2012"},{"key":"296_CR23","unstructured":"Giffin DB, Levy A, Stefan D, Terei D, Mazi\u00e8res D, Mitchell JC, Russo A (2012) Hails: protecting data privacy in untrusted web applications. In: OSDI"},{"issue":"3","key":"296_CR24","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"296_CR25","unstructured":"Gudka K, Watson RNM, Hand S, Laurie B, Madhavapeddy A (2012) Exploring compartmentalization hypothesis with SOAPP. In: AHANS 2012"},{"key":"296_CR26","unstructured":"Harris W (2014) Secure programming via game-based synthesis. PhD thesis, University of Wisconsin\u2014Madison"},{"key":"296_CR27","unstructured":"Harris W, Zeldovich N, Jha S, Reps T, Manevich R, Sagiv M (2014) Modular synthesis of DIFC programs. Technical report, Georgia Insitute of Technology"},{"key":"296_CR28","doi-asserted-by":"crossref","unstructured":"Harris WR, Jha S, Reps T (2010) DIFC programs by automatic instrumentation. In: CCS","DOI":"10.1145\/1866307.1866340"},{"key":"296_CR29","doi-asserted-by":"crossref","unstructured":"Harris WR, Jha S, Reps T (2012) Secure programming via visibly pushdown safety games. In: CAV","DOI":"10.1007\/978-3-642-31424-7_41"},{"key":"296_CR30","doi-asserted-by":"crossref","unstructured":"Harris WR, Jha S, Reps T, Anderson J, Watson RNM (2013) Declarative, temporal, and practical programming with capabilities. In: SSP","DOI":"10.1109\/SP.2013.11"},{"key":"296_CR31","doi-asserted-by":"crossref","unstructured":"Hawkins P, Aiken A, Fisher K, Rinard MC, Sagiv M (2011) Data representation synthesis. In: PLDI","DOI":"10.1145\/1993498.1993504"},{"key":"296_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14303-8","volume-title":"Efficient secure two-party protocols: techniques and constructions","author":"C Hazay","year":"2010","unstructured":"Hazay C, Lindell Y (2010) Efficient secure two-party protocols: techniques and constructions. Springer, Berlin"},{"key":"296_CR33","doi-asserted-by":"crossref","unstructured":"Holzer A, Franz M, Katzenbeisser S, Veith H (2012) Secure two-party computations in ANSI C. In: CCS","DOI":"10.1145\/2382196.2382278"},{"key":"296_CR34","doi-asserted-by":"crossref","unstructured":"Hri\u0163cu C, Greenberg M, Karel B, Pierce BC, Morrisett G (2013) All your IFCException are belong to us. In: SSP","DOI":"10.1109\/SP.2013.10"},{"key":"296_CR35","unstructured":"Intel Software (2016) Intel SGX homepage. \n                    https:\/\/software.intel.com\/en-us\/sgx\n                    \n                  . Accessed 9 Sept 2016"},{"key":"296_CR36","doi-asserted-by":"crossref","unstructured":"Jobstmann B, Griesmayer A, Bloem R (2005) Program repair as a game. In: CAV","DOI":"10.1007\/11513988_23"},{"key":"296_CR37","doi-asserted-by":"crossref","unstructured":"Krohn MN, Yip A, Brodsky MZ, Cliffer N, Kaashoek MF, Kohler E, Morris R (2007) Information flow control for standard OS abstractions. In: SOSP","DOI":"10.1145\/1294261.1294293"},{"key":"296_CR38","unstructured":"Lattner C (2011) \n                    http:\/\/llvm.org\/\n                    \n                  , Nov 2011"},{"key":"296_CR39","doi-asserted-by":"crossref","unstructured":"Livshits B, Chong S (2013) Towards fully automatic placement of security sanitizers and declassifiers. In: POPL","DOI":"10.1145\/2429069.2429115"},{"key":"296_CR40","doi-asserted-by":"crossref","unstructured":"Livshits VB, Nori AV, Rajamani SK, Banerjee A (2009) Merlin: specification inference for explicit information flow problems. In: PLDI","DOI":"10.1145\/1542476.1542485"},{"key":"296_CR41","unstructured":"Manevich R (2011) \n                    http:\/\/www.cs.tau.ac.il\/tvla\n                    \n                  , June 2011"},{"key":"296_CR42","doi-asserted-by":"crossref","unstructured":"Myers AC (1999) Jflow: practical mostly-static information flow control. In: POPL","DOI":"10.1145\/292540.292561"},{"key":"296_CR43","unstructured":"Neumann PG, Boyer RS, Robinson L, Levitt KN, Boyer RS, Saxena AR (1980) A provably secure operating system. Technical report CSL-116, Stanford Research Institute"},{"key":"296_CR44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"In transition from global to modular temporal reasoning about programs","author":"A Pnueli","year":"1985","unstructured":"Pnueli A (1985) Logics and models of concurrent systems. In: Apt KR (ed) In transition from global to modular temporal reasoning about programs. Springer, New York"},{"key":"296_CR45","doi-asserted-by":"crossref","unstructured":"Roy I, Porter DE, Bond MD, McKinley KS, Witchel E (2009) Laminar: practical fine-grained decentralized information flow control. In: PLDI","DOI":"10.1145\/1542476.1542484"},{"key":"296_CR46","doi-asserted-by":"crossref","unstructured":"Sabelfeld A, Sands D (2005) Dimensions and principles of declassification. In: CSFW-18","DOI":"10.1109\/CSFW.2005.15"},{"issue":"3","key":"296_CR47","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv S, Reps T, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217\u2013298","journal-title":"ACM Trans Program Lang Syst"},{"issue":"9","key":"296_CR48","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1109\/PROC.1975.9939","volume":"63","author":"JH Saltzer","year":"1975","unstructured":"Saltzer JH, Schroeder MD (1975) The protection of information in computer systems. Proc IEEE 63(9):1278\u20131308","journal-title":"Proc IEEE"},{"key":"296_CR49","doi-asserted-by":"crossref","unstructured":"Schuster F, Costa M, Fournet C, Gkantsidis C, Peinado M, Mainar-Ruiz G, Russinovich M (2015) VC3: trustworthy data analytics in the cloud using SGX. In: SP","DOI":"10.1109\/SP.2015.10"},{"key":"296_CR50","doi-asserted-by":"crossref","unstructured":"Shapiro JS, Smith JM, Farber DJ (1999) EROS: a fast capability system. In: SOSP","DOI":"10.1145\/319151.319163"},{"key":"296_CR51","doi-asserted-by":"crossref","unstructured":"Sinha R, Costa M, Lal A, Lopes NP, Rajamani SK, Seshia SA, Vaswani K (2016) A design and verification methodology for secure isolated regions. In: PLDI","DOI":"10.1145\/2908080.2908113"},{"key":"296_CR52","doi-asserted-by":"crossref","unstructured":"Sinha R, Rajamani SK, Seshia SA, Vaswani K (2015) Moat: verifying confidentiality of enclave programs. In: CCS","DOI":"10.1145\/2810103.2813608"},{"key":"296_CR53","doi-asserted-by":"crossref","unstructured":"Skalka C, Smith SF (2000) Static enforcement of security with types. In: ICFP, pp 34\u201345","DOI":"10.1145\/351240.351244"},{"key":"296_CR54","doi-asserted-by":"crossref","unstructured":"Sohail S, Somenzi F (2009) Safety first: a two-stage algorithm for LTL games. In: FMCAD","DOI":"10.1109\/FMCAD.2009.5351138"},{"key":"296_CR55","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Arnold G, Tancau L, Bod\u00edk R, Saraswat VA, Seshia SA (2007) Sketching stencils. In: PLDI","DOI":"10.1145\/1250734.1250754"},{"key":"296_CR56","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Jones CG, Bod\u00edk R (2008) Sketching concurrent data structures. In: PLDI","DOI":"10.1145\/1375581.1375599"},{"key":"296_CR57","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Rabbah RM, Bod\u00edk R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: PLDI","DOI":"10.1145\/1065010.1065045"},{"key":"296_CR58","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Tancau L, Bod\u00edk R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: ASPLOS","DOI":"10.1145\/1168857.1168907"},{"key":"296_CR59","doi-asserted-by":"crossref","unstructured":"Swamy N, Chen J, Fournet C, Strub P-Y, Bhargavan K, Yang J (2011) Secure distributed programming with value-dependent types. In: ICFP","DOI":"10.1145\/2034773.2034811"},{"key":"296_CR60","doi-asserted-by":"crossref","unstructured":"Swamy N, Corcoran BJ, Hicks M (2008) Fable: a language for enforcing user-defined security policies. In: SSP","DOI":"10.1109\/SP.2008.29"},{"issue":"12","key":"296_CR61","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1513443.1513448","volume":"43","author":"N Swamy","year":"2008","unstructured":"Swamy N, Hicks M (2008) Verified enforcement of stateful information release policies. SIGPLAN Not 43(12):21\u201331","journal-title":"SIGPLAN Not"},{"key":"296_CR62","unstructured":"T. M. Corporation (2011) Cwe\u20142011 cwe\/sans top 25 most dangerous software errors"},{"key":"296_CR63","doi-asserted-by":"crossref","unstructured":"Tsai M-H, Tsay Y-K, Hwang Y-S (2013) GOAL for games, omega-automata, and logics. In: CAV","DOI":"10.1007\/978-3-642-39799-8_62"},{"key":"296_CR64","unstructured":"U.S.D. of Defense. Trusted computer system evaluation criteria. DoD Standard 5200.28-STD, Dec 1985"},{"key":"296_CR65","doi-asserted-by":"crossref","unstructured":"Vaughan JA, Chong S (2011) Inference of expressive declassification policies. In: SSP","DOI":"10.1109\/SP.2011.20"},{"key":"296_CR66","unstructured":"Vulnerability note VU#520827. \n                    http:\/\/www.kb.cert.org\/vuls\/id\/520827\n                    \n                  , May 2012"},{"key":"296_CR67","unstructured":"Vulnerability note VU#381508. \n                    http:\/\/www.kb.cert.org\/vuls\/id\/381508\n                    \n                  , July 2011"},{"key":"296_CR68","unstructured":"Watson RNM, Anderson J, Laurie B, Kennaway K (2010) Capsicum: practical capabilities for UNIX. In: USENIX security symposium"},{"key":"296_CR69","unstructured":"Wright C, Cowan C, Smalley S, Morris J, Kroah-Hartman G (2002) Linux security modules: general security support for the Linux kernel. In: USENIX security symposium"},{"key":"296_CR70","doi-asserted-by":"crossref","unstructured":"Yao A (1982) Protocols for secure computations. In: FOCS","DOI":"10.1109\/SFCS.1982.38"},{"key":"296_CR71","unstructured":"Zeldovich N, Boyd-Wickizer S, Kohler E, Mazi\u00e8res D (2006) Making information flow explicit in HiStar. In: OSDI"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0296-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0296-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0296-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:45:03Z","timestamp":1589730303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0296-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,16]]},"references-count":71,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["296"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0296-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,9,16]]},"assertion":[{"value":"16 September 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}