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

Harris, William R.; Jha, Somesh; Reps, Thomas W.; Seshia, Sanjit A.

Form. Methods Syst. Des. 51, No. 2, 362-394 (2017).

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.

MSC:

68N30

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Keywords:

computer security; program synthesis; information flow; capabilities; secure isolated regions

Software:

EROS; SGX; VC3; Moat; Merlin; Privtrans; F*; Laminar; Fable; JFlow; LLVM

References:

[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
[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
[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
[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
[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
[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
[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
[48]	Saltzer JH, Schroeder MD (1975) The protection of information in computer systems. Proc IEEE 63(9):1278-1308
[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
[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