×

Compiling information-flow security to minimal trusted computing bases. (English) Zbl 1326.68075

Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 216-235 (2011).
Summary: Information-flow policies can express strong security requirements for programs run by distributed parties with different levels of trust. However, this security is hard to preserve as programs get compiled to distributed systems with (potentially) compromised machines. For instance, many programs involve computations too sensitive to be trusted to any of those machines. Also, many programs are not perfectly secure (non-interferent); as they selectively endorse and declassify information, their relative security becomes harder to preserve.
We develop a secure compiler for distributed information flows. To minimize trust assumptions, we rely on cryptographic protection, and we exploit hardware and software mechanisms available on modern architectures, such as secure boots, trusted platform modules, and remote attestation.
We present a security model for these mechanisms in an imperative language with dynamic code loading. We define program transformations to generate trusted virtual hosts and to run them on untrusted machines. We obtain confidentiality and integrity theorems under realistic assumptions, showing that the compiled distributed system is at least as secure as the source program.
For the entire collection see [Zbl 1213.68027].

MSC:

68N20 Theory of compilers and interpreters
68N15 Theory of programming languages

Software:

Flicker; Jif
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Wobber, T.: A logical account of NGSCB. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 1–12. Springer, Heidelberg (2004) · Zbl 1110.68308 · doi:10.1007/978-3-540-30232-2_1
[2] AMD. AMD64 virtualization: Secure virtual machine architecture reference manual
[3] Askarov, A., Myers, A.: A semantic framework for declassification and endorsement. Prog. Languages and Systems, 64–84 (2010) · Zbl 1260.68049
[4] Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF (2009) · doi:10.1109/CSF.2009.22
[5] Balfe, S., Paterson, K.G.: e-EMV: Emulating EMV for internet payments using trusted computing technology. In: STC 2008, pp. 81–92 (2008)
[6] Chong, S., Myers, A.C.: Decentralized robustness. In: 19th IEEE CSFW 2006, p. 12 (2006) · doi:10.1109/CSFW.2006.11
[7] Chong, S., Liu, J., Myers, A.C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning. In: CACM (2009)
[8] Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: S&P 2009, pp. 221–236 (2009) · doi:10.1109/SP.2009.16
[9] Denning, D.E.: A lattice model of secure information flow. In: CACM (1976) · Zbl 0322.68034
[10] Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE TIT (1976) · Zbl 0435.94018
[11] Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: POPL 2008, pp. 323–335 (January 2008) · Zbl 1295.94065 · doi:10.1145/1328438.1328478
[12] Fournet, C., Le Guernic, G., Rezk, T.: A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms. In: CCS 2009, ACM, New York (2009)
[13] Grawrock, D.: TCG Specification Architecture Overview, Rev. 1.4 (2007)
[14] Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security evaluation of scenarios based on the TCGs TPM specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007) · Zbl 05314742 · doi:10.1007/978-3-540-74835-9_29
[15] Halderman, J., Schoen, S., Heninger, N., Clarkson, W., Paul, W., Calandrino, J., Feldman, A., Appelbaum, J., Felten, E.: Lest we remember: cold-boot attacks on encryption keys. In: CACM (2009)
[16] Intel. Intel Trusted Execution Technology Software Development Guide (2009)
[17] McCune, J., Parno, B., Perrig, A., Reiter, M., Isozaki, H.: Flicker: An execution infrastructure for TCB minimization. In: 3rd ACM SIGOPS/EuroSys, pp. 315–328. ACM, New York (2008)
[18] McCune, J., Qu, N., Li, Y., Datta, A., Gligor, V., Perrig, A.: Efficient TCB Reduction and Attestation. CMU-CyLab-09-003 9 (2009)
[19] Microsoft. Windows BitLocker drive encryption (2006)
[20] Millen, J., Guttman, J., Ramsdell, J., Sheehy, J., Sniffen, B., Bedford, M.: Analysis of a measured launch. In: MITRE (2007)
[21] Myers, A.C., Liskov, B.: Complete, safe information flow with decentralized labels. In: 19th IEEE Symposium on Research in Security and Privacy (RSP), Oakland, California (May 1998) · doi:10.1109/SECPRI.1998.674834
[22] Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. In: TOSEM (2000)
[23] Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow (2001)
[24] Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. JCS 14(2), 157–196 (2006) · Zbl 05430417 · doi:10.3233/JCS-2006-14203
[25] Pottier, F., Simonet, V.: Information flow inference for ML. In: ACM TOPLAS (2003) · Zbl 05459321 · doi:10.1145/596980.596983
[26] Sabelfeld, A., Myers, A.C.: Language-based information-flow security. In: IEEE J-SAC (2003) · doi:10.1109/JSAC.2002.806121
[27] Sabelfeld, A., Myers, A.C.: A model for delimited information release. Software Security-Theories and Systems, 174–191 (2004)
[28] Trusted Computing Group. Client Specific TPM Interface Specification (TIS), Version 1.2 (2005)
[29] Trusted Computing Group. TCG Software Stack (TSS 1.2). Trusted Computing Group (2006)
[30] Zdancewic, S., Myers, A.C.: Robust declassification. In: CSFW 2001, pp. 15–23 (2001) · doi:10.1109/CSFW.2001.930133
[31] Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program partitioning. In: TOCS (2002)
[32] Zheng, L., Chong, S., Myers, A.C., Zdancewic, S.: Using replication and partitioning to build secure distributed systems. In: 15th IEEE Symposium on Security and Privacy (2003)
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.