Program synthesis for interactive-security systems. (English) Zbl 1386.68032

Summary: Developing practical but secure programs remains an important and open problem. Recently, the operating-system and architecture communities have proposed novel systems, which we refer to as interactive-security systems. They provide primitives that a program can use to perform security-critical operations, such as reading from and writing to system storage by restricting some modules to execute with limited privileges. Developing programs that use the low-level primitives provided by such systems to correctly ensure end-to-end security guarantees while preserving intended functionality is a challenging problem. This paper describes previous and proposed work on techniques and tools that enable a programmer to generate programs automatically that use such primitives. For two interactive security systems, namely the Capsicum capability system and the HiStar information-flow system, we developed languages of policies that a programmer can use to directly express security and functionality requirements, along with synthesizers that take a program and policy in the language and generate a program that correctly uses system primitives to satisfy the policy. We propose future work on developing a similar synthesizer for novel architectures that enable an application to execute different modules in Secure Isolated Regions without trusting any other software components on a platform, including the operating system.


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI Link


[1] Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: CAV
[2] Alur R, Bodík 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
[3] Alur R, La Torre S, Madhusudan P (2006) Modular strategies for recursive game graphs. Theor Comput Sci 354(2):230-249 · Zbl 1088.68099 · doi:10.1016/j.tcs.2005.11.017
[4] Alur R, Madhusudan P (2004) Visibly pushdown languages. In: STOC · Zbl 1192.68396
[5] ARM (2016) Products. https://www.arm.com/products/security-on-arm/trustzone. Accessed 9 Sept 2016 · Zbl 1088.68099
[6] Barthe G, Fournet C, Grégoire B, Strub P-Y, Swamy N, Béguelin SZ (2014) Probabilistic relational verification for cryptographic implementations. In: POPL · Zbl 1284.68380
[7] Bittau A, Marchenko P, Handley M, Karp B (2008) Wedge: splitting applications into reduced-privilege compartments. In: NSDI
[8] Brumley D, Song D X (2004) Privtrans: automatically partitioning programs for privilege separation. In: USENIX security symposium
[9] C. E. Board. CVE-2007-4476. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2007-4476, Aug 2007
[10] C. E. Board. GNU Tar and GNU Cpio rmt_read__() function buffer overflow. http://xforce.iss.net/xforce/xfdb/56803, Mar 2010
[11] Cheung A, Arden O, Madden S, Myers AC (2012) Automatic partitioning of database applications. PVLDB 5(11):1471-1482
[12] Chong S, Liu J, Myers A C, Qi X, Vikram K, Zheng L, Zheng X (2007) Secure web application via automatic partitioning. In: SOSP
[13] Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157-1210 · doi:10.3233/JCS-2009-0393
[14] Costan V, Lebedev I, Devadas S (2015) Sanctum: minimal hardware extensions for strong software isolation. Cryptology ePrint Archive, Report 2015/564. http://eprint.iacr.org/
[15] CVE-2004-1488. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CAN-2004-1488, Feb 2005
[16] CVE-2007-3798. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2007-3798, July 2007
[17] CVE-2010-0405. http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2010-0405, Apr 2010
[18] Denning DE (1976) A lattice model of secure information flow. Commun ACM 19(5):236-243 · Zbl 0322.68034 · doi:10.1145/360051.360056
[19] Efstathopoulos P, Kohler E (2008) Manageable fine-grained information flow. In: EuroSys
[20] Efstathopoulos P, Krohn M N, Vandebogart S, Frey C, Ziegler D, Kohler E, Mazières D, Kaashoek MF, Morris R (2005) Labels and event processes in the Asbestos operating system. In: SOSP
[21] Erlingsson Ú, Schneider FB (2000) IRM enforcement of Java stack inspection. In: SSP
[22] FreeBSD 9.0-RELEASE announcement. http://www.freebsd.org/releases/9.0R/announce.html, Jan 2012
[23] Giffin DB, Levy A, Stefan D, Terei D, Mazières D, Mitchell JC, Russo A (2012) Hails: protecting data privacy in untrusted web applications. In: OSDI
[24] Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843-871 · doi:10.1145/177492.177725
[25] Gudka K, Watson RNM, Hand S, Laurie B, Madhavapeddy A (2012) Exploring compartmentalization hypothesis with SOAPP. In: AHANS 2012
[26] Harris W (2014) Secure programming via game-based synthesis. PhD thesis, University of Wisconsin—Madison
[27] Harris W, Zeldovich N, Jha S, Reps T, Manevich R, Sagiv M (2014) Modular synthesis of DIFC programs. Technical report, Georgia Insitute of Technology
[28] Harris WR, Jha S, Reps T (2010) DIFC programs by automatic instrumentation. In: CCS
[29] Harris WR, Jha S, Reps T (2012) Secure programming via visibly pushdown safety games. In: CAV
[30] Harris WR, Jha S, Reps T, Anderson J, Watson RNM (2013) Declarative, temporal, and practical programming with capabilities. In: SSP
[31] Hawkins P, Aiken A, Fisher K, Rinard MC, Sagiv M (2011) Data representation synthesis. In: PLDI
[32] Hazay C, Lindell Y (2010) Efficient secure two-party protocols: techniques and constructions. Springer, Berlin · Zbl 1208.68005 · doi:10.1007/978-3-642-14303-8
[33] Holzer A, Franz M, Katzenbeisser S, Veith H (2012) Secure two-party computations in ANSI C. In: CCS
[34] Hriţcu C, Greenberg M, Karel B, Pierce BC, Morrisett G (2013) All your IFCException are belong to us. In: SSP
[35] Intel Software (2016) Intel SGX homepage. https://software.intel.com/en-us/sgx. Accessed 9 Sept 2016
[36] Jobstmann B, Griesmayer A, Bloem R (2005) Program repair as a game. In: CAV · Zbl 1081.68572
[37] Krohn MN, Yip A, Brodsky MZ, Cliffer N, Kaashoek MF, Kohler E, Morris R (2007) Information flow control for standard OS abstractions. In: SOSP
[38] Lattner C (2011) http://llvm.org/, Nov 2011
[39] Livshits B, Chong S (2013) Towards fully automatic placement of security sanitizers and declassifiers. In: POPL · Zbl 1301.68093
[40] Livshits VB, Nori AV, Rajamani SK, Banerjee A (2009) Merlin: specification inference for explicit information flow problems. In: PLDI
[41] Manevich R (2011) http://www.cs.tau.ac.il/tvla, June 2011
[42] Myers AC (1999) Jflow: practical mostly-static information flow control. In: POPL
[43] 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
[44] Pnueli, A.; Apt, KR (ed.), Logics and models of concurrent systems (1985), New York · doi:10.1007/978-3-642-82453-1_5
[45] Roy I, Porter DE, Bond MD, McKinley KS, Witchel E (2009) Laminar: practical fine-grained decentralized information flow control. In: PLDI
[46] Sabelfeld A, Sands D (2005) Dimensions and principles of declassification. In: CSFW-18
[47] Sagiv S, Reps T, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217-298 · doi:10.1145/514188.514190
[48] Saltzer JH, Schroeder MD (1975) The protection of information in computer systems. Proc IEEE 63(9):1278-1308 · doi:10.1109/PROC.1975.9939
[49] 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
[50] Shapiro JS, Smith JM, Farber DJ (1999) EROS: a fast capability system. In: SOSP
[51] 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
[52] Sinha R, Rajamani SK, Seshia SA, Vaswani K (2015) Moat: verifying confidentiality of enclave programs. In: CCS
[53] Skalka C, Smith SF (2000) Static enforcement of security with types. In: ICFP, pp 34-45 · Zbl 1088.68099
[54] Sohail S, Somenzi F (2009) Safety first: a two-stage algorithm for LTL games. In: FMCAD
[55] Solar-Lezama A, Arnold G, Tancau L, Bodík R, Saraswat VA, Seshia SA (2007) Sketching stencils. In: PLDI
[56] Solar-Lezama A, Jones CG, Bodík R (2008) Sketching concurrent data structures. In: PLDI · Zbl 0322.68034
[57] Solar-Lezama A, Rabbah RM, Bodík R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: PLDI
[58] Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: ASPLOS
[59] Swamy N, Chen J, Fournet C, Strub P-Y, Bhargavan K, Yang J (2011) Secure distributed programming with value-dependent types. In: ICFP · Zbl 1323.68229
[60] Swamy N, Corcoran BJ, Hicks M (2008) Fable: a language for enforcing user-defined security policies. In: SSP
[61] Swamy N, Hicks M (2008) Verified enforcement of stateful information release policies. SIGPLAN Not 43(12):21-31 · doi:10.1145/1513443.1513448
[62] T. M. Corporation (2011) Cwe—2011 cwe/sans top 25 most dangerous software errors
[63] Tsai M-H, Tsay Y-K, Hwang Y-S (2013) GOAL for games, omega-automata, and logics. In: CAV
[64] U.S.D. of Defense. Trusted computer system evaluation criteria. DoD Standard 5200.28-STD, Dec 1985
[65] Vaughan JA, Chong S (2011) Inference of expressive declassification policies. In: SSP
[66] Vulnerability note VU#520827. http://www.kb.cert.org/vuls/id/520827, May 2012
[67] Vulnerability note VU#381508. http://www.kb.cert.org/vuls/id/381508, July 2011
[68] Watson RNM, Anderson J, Laurie B, Kennaway K (2010) Capsicum: practical capabilities for UNIX. In: USENIX security symposium
[69] 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
[70] Yao A (1982) Protocols for secure computations. In: FOCS
[71] Zeldovich N, Boyd-Wickizer S, Kohler E, Mazières D (2006) Making information flow explicit in HiStar. In: OSDI
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.