Martín Abadi
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Layout randomization is a powerful, popular technique for software protection. We present it and study it in programming-language terms. More specifically, we consider layout randomization as part of an implementation for a high-level programming language; the implementation translates this language to a lower-level language in which memory addresses are numbers. We analyze this implementation, by relating low-level attacks against the implementation to contexts in the high-level programming language, and by establishing full abstraction results.
Supplemental Material
Available for Download
pdf
a8-abadi_appendix.pdf (113.1 KB)
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- Abadi, M. 1998. Protection in programming-language translations. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 1443. Springer, 868--883. Google Scholar
Digital Library
- Abadi, M. 1999. Secrecy by typing in security protocols. J. ACM 46, 5, 749--786. Google ScholarDigital Library
- Abadi, M. and Rogaway, P. 2002. Reconciling two views of cryptography (The computational soundness of formal encryption). J. Crypt. 15, 2, 103--127. Google ScholarDigital Library
- Abadi, M., Budiu, M., Erlingsson, U., and Ligatti, J. 2009. Control-flow integrity: Principles, implementations, and applications. ACM Trans. Info. Syst. Security 13, 1, 1--40. Google ScholarDigital Library
- Anonymous. 2002. Bypassing PaX ASLR protection. Phrack 11, 59.Google Scholar
- Backes, M., Hofheinz, D., and Unruh, D. 2009. CoSP: A general framework for computational soundness proofs. In Proceedings of the 16th ACM Conference on Computer and Communications Security. 66--78. Google ScholarDigital Library
- Barrantes, E. G., Ackley, D. H., Forrest, S., and Stefanović, D. 2005. Randomized instruction set emulation. ACM Trans. Inf. Syst. Sec. 8, 1, 3--40. Google ScholarDigital Library
- Barthe, G., Rezk, T., and Basu, A. 2007. Security types preserving compilation. Comput. Lang. Syst. Struct. 33, 2, 35--59. Google ScholarDigital Library
- Berger, E. D. and Zorn, B. G. 2006. DieHard: Probabilistic memory safety for unsafe languages. In Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. 158--168. Google ScholarDigital Library
- Bhatkar, S., DuVarney, D. C., and Sekar, R. 2003. Address obfuscation: An efficient approach to combat a broad range of memory error exploits. In Proceedings of the 12th USENIX Security Symposium. Google ScholarDigital Library
- Bhatkar, S., Sekar, R., and DuVarney, D. C. 2005. Efficient techniques for comprehensive protection from memory error exploits. In Proceedings of the 14th USENIX Security Symposium. Google ScholarDigital Library
- Chen, S., Jun Xu, E. C. S., Gauriar, P., and Iyer, R. K. 2005. Non-control-data attacks are realistic threats. In Proceedings of the Usenix Security Symposium. 177--192. Google ScholarDigital Library
- Comon-Lundh, H. and Cortier, V. 2008. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security. 109--118. Google ScholarDigital Library
- Denning, D. E. 1982. Cryptography and Data Security. Addison-Wesley, Reading, Mass.Google Scholar
- Druschel, P. and Peterson, L. L. 1992. High-performance cross-domain data transfer. Tech. rep. TR 92-11, Department of Computer Science, The University of Arizona.Google Scholar
- Erlingsson, Ú. 2007. Low-level software security: Attacks and defenses. In Proceedings of the Foundations of Security Analysis and Design IV, FOSAD 2006/2007 Tutorial Lectures, A. Aldini and R. Gorrieri Eds., Lecture Notes in Computer Science, vol. 4677. Springer, 92--134. Google ScholarDigital Library
- Felleisen, M. and Friedman, D. P. 1986. Control operators, the secd-machine, and the lambda-calculus. In Proceedings of the 3rd Working Conference on the Formal Description of Programming Concepts. 193--219.Google Scholar
- Forrest, S., Somayaji, A., and Ackley, D. H. 1997. Building diverse computer systems. In Proceedings of the 6th Workshop on Hot Topics in Operating Systems. 67--72. Google ScholarDigital Library
- Fournet, C. and Rezk, T. 2008. Cryptographically sound implementations for typed information-flow security. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 323--335. Google ScholarDigital Library
- Fournet, C., Guernic, G. L., and Rezk, T. 2009. A security-preserving compiler for distributed programs: From information-flow policies to cryptographic mechanisms. In Proceedings of the 16th ACM Conference on Computer and Communications Security. 432--441. Google ScholarDigital Library
- Hasegawa, M. and Kakutani, Y. 2002. Axioms for recursion in call-by-value. Higher-Order Symbolic Comput. 15, 2-3, 235--264. Google ScholarDigital Library
- Howard, M. and Thomlinson, M. 2007. Windows Vista ISV security. http://msdn2.microsoft.com/en-us/library/bb430720.aspx.Google Scholar
- Kc, G. S., Keromytis, A. D., and Prevelakis, V. 2003. Countering code-injection attacks with instruction-set randomization. In Proceedings of the 10th ACM Conference on Computer and Communications security. 272--280. Google ScholarDigital Library
- Kiriansky, V., Bruening, D., and Amarasinghe, S. 2002. Secure execution via program shepherding. In Proceedings of the 11th USENIX Security Symposium. 191--206. Google ScholarDigital Library
- Medel, R. H. 2006. Typed assembly languages for software security. Ph.D. dissertation, Stevens Institute of Technology. Google ScholarDigital Library
- Mitchell, J. 1996. Foundations for Programming Languages. MIT Press. Google ScholarDigital Library
- Moggi, E. 1989. Computational lambda-calculus and monads. In Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science. 14--23. Google ScholarDigital Library
- Moggi, E. 1991. Notions of computation and monads. Inf. Comput. 93, 1, 55--92. Google ScholarDigital Library
- Morris Jr., J. H. 1973. Protection in programming languages. Comm. ACM 16, 1, 15--21. Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999. From System F to typed assembly language. ACM Trans. Prog. Lang. Syst. 21, 3, 527--568. Google ScholarDigital Library
- Novark, G. and Berger, E. D. 2010. DieHarder: Securing the heap. In Proceedings of the 17th ACM Conference on Computer and Communications security. 573--584. Google ScholarDigital Library
- Novark, G., Berger, E. D., and Zorn, B. G. 2008. Exterminator: Automatically correcting memory errors with high probability. Comm. ACM 51, 12, 87--95. Google ScholarDigital Library
- Pattabiraman, K., Grover, V., and Zorn, B. G. 2008. Samurai: Protecting critical data in unsafe languages. In Proceedings of EuroSys. 219--232. Google ScholarDigital Library
- PaX Project. 2004. The PaX project. http://pax.grsecurity.net/.Google Scholar
- Pierce, B. 2002. Types and Programming Languages. MIT Press. Google ScholarDigital Library
- Pucella, R. and Schneider, F. B. 2006. Independence from obfuscation: A semantic framework for diversity. In Proceedings of the 19th IEEE Computer Security Foundations Workshop. 230--241. Google ScholarDigital Library
- Shacham, H., Page, M., Pfaff, B., Goh, E.-J., Modadugu, N., and Boneh, D. 2004. On the effectiveness of address-space randomization. In Proceedings of the 11th ACM Conference on Computer and Communications Security. 298--307. Google ScholarDigital Library
- Sotirov, A. and Dowd, M. 2008. Bypassing browser memory protections: Setting back browser security by 10 years. http://taossa.com/archive/bh08sotirovdowd.pdf.Google Scholar
- Sovarel, A. N., Evans, D., and Paul, N. 2005. Where’s the FEEB? the effectiveness of instruction set randomization. In Proceedings of the 14th USENIX Security Symposium. 145--160. Google ScholarDigital Library
- Volpano, D., Irvine, C., and Smith, G. 1996. A sound type system for secure flow analysis. J. Comput. Sec. 4, 167--187. Google ScholarDigital Library
- Yarvin, C., Bukowski, R., and Anderson, T. 1993. Anonymous RPC: Low-latency protection in a 64-bit address space. In Proceedings of the USENIX Summer Technical Conference. 175--186. Google ScholarDigital Library
Index Terms
- On Protection by Layout Randomization
Recommendations
On Protection by Layout Randomization
CSF '10: Proceedings of the 2010 23rd IEEE Computer Security Foundations SymposiumLayout randomization is a powerful, popular technique for software protection. We present it and study it in programming-language terms. More specifically, we consider layout randomization as part of an implementation for a highlevel programming ...
On the General Applicability of Instruction-Set Randomization
We describe Instruction-Set Randomization (ISR), a general approach for safeguarding systems against any type of code-injection attack. We apply Kerckhoffs' principle to create OS process-specific randomized instruction sets (e.g., machine instructions) ...
Return address randomization scheme for annuling data-injection buffer overflow attacks
Inscrypt'06: Proceedings of the Second SKLOIS conference on Information Security and CryptologyBuffer overflow(BOF) has been the most common form of vulnerability in software systems today, and many methods exist to defend software systems against BOF attacks. Among them, the instruction set randomization scheme, which makes attacker not to know ...
Comments