Language-Based Security 
for 
Malicious Mobile Code

The project is supported in part by the Office of Naval Research's Critical Infrastructure Protection and High Confidence, Adaptable Software (CIP/SW) initiative and Intel.

Principal Investigators:

Fred B. Schneider	Dexter Kozen
Computer Science Department	Computer Science Department
4115C Upson Hall	5143 Upson Hall
Cornell University	Cornell University
Ithaca, New York  14853-7501	Ithaca, New York  14853-7501
Tel:  (607) 255-9221	Tel:  (607) 255-9209
Fax: (607) 255-4428	Fax: (607) 255-4428
fbs@cs.cornell.edu	kozen@cs.cornell.edu
Greg Morrisett	Andrew Myers
Computer Science Department	Computer Science Department
327 Maxwell Dworkin	Upson Hall
Harvard University	Cornell University
Cambridge, MA  02138	Ithaca, New York  14853-7501
Tel: (617) 495-9526	Tel: (607) 255-8597
Fax: (607) 255-4428	Fax: (607) 255-4428
	andru@cs.cornell.edu

Project Overview:

Mobile code provides a convenient, efficient, and economical way to extend the functionality and improve the performance of networked computing systems. It is an approach that has been widely embraced, as evidenced by today's operating systems, web browsers, and applications with their support for "plug-and-play", Javascript, downloaded helper applications, and executable attachments. Yet today's security architectures provide poor protection from faulty, much less from malicious, extensions. Our information systems are thus increasingly susceptible to attacks—attacks that can have devastating consequences.

The Language-Based Security project at Cornell University aims to develop and refine new security enforcement mechanisms that are well suited for networked computing systems built from extensible components.  Our work is broad in scope but has a common theme—leveraging recent developments in the field of programming languages while building on classic computer security principles. 

Our research leverages programming language technology including:

• in-lined reference monitors 
• flexible, type-based enforcement of information flow policies 
• typed assembly language, type-safe systems languages such as C, 
• proof-carrying code, and
• efficient certifying compilers. 

Many of these technologies were developed here at Cornell.  Our current work seeks to move these technologies from the lab to real-world settings, and to explore the synergistic combination of advanced language technologies in the deployment of next-generation security architectures.  We thus expect to develop the efficient and powerful means needed for enforcing the wide range of security policies required in extensible systems.

Software:

• TAL:  Typed Assembly Language
  
• Jif:  Java + Information Flow
  
• Cyclone:  A Type-Safe Dialect of C
  
• ECC:  Efficient Code Certification
• PittSFIeld
  

Graduate and Post Doctoral Students:

• Amal Ahmed (Post Doc)
• James Cheney (now at Univ. of Edinburgh)
• Stephen Chong
• Michael Clarkson
• Matthew Fluet
• Dan Grossman (now at Univ. of Washington)
• Kevin Hamlen
• Mike Hicks (Post Doc, now at Univ. of Maryland)
• Jed Liu
• Nathaniel Nystrom
• Yanling Wang
• Stephanie Weirich (now at Univ. of Pennsylvania)
• Lantian Zheng

Courses:

• Cornell CS513 Spring 2004: System Security
• Harvard CS255 Spring 2004: Topics in Language-Based Security
• Cornell CS711 Fall 2003: Topics in Language-Based Security
• Cornell CS711 Fall 2002: Topics in Language-Based Security
• Cornell CS513 Spring 2002: System Security
• Cornell CS711 Spring 2002: Topics in Language-Based Security

Related Publications from the Group:

General:

• Fred B. Schneider. Least Privilege and More IEEE Security and Privacy Magazine, Volume 1, Number 5, (September/October 2003), 55-59.
• Fred B. Schneider, Greg Morrisett, Robert Harper. A language-based approach to security. Informatics: 10 Years Back, 10 Years Ahead, Lecture Notes in Computer Science, Vol. 2000, Springer-Verlag, Heidelberg, 86-101.
• McGraw, Gary and Greg Morrisett. Attacking malicious code: a report to the Infosec Research Council. In IEEE Software, Volume 17(5), September/October 2000.
• Dexter Kozen.  "Language-based security," In M. Kutylowski, L. Pacholski, and T. Wierzbicki, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99), Lecture Notes in Computer Science v. 1672, Springer-Verlag, September 1999, 284-298.

Security Automata and Inlined Reference Monitors:

• Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. Computability classes for enforcement mechanisms. To appear in ACM Transactions on Programming Languages and Systems. Also available as Cornell Computer Science Department Technical Report TR2003-1908, August 2003.
• Stephen McCamant and Greg Morrisett.   Efficient, Verifiable Binary Sandboxing for a CISC Architecture. MIT Laboratory for Computer Science Technical Report 988 (MIT-LCS-TR-988). May 2nd, 2005. [Postscript] [PDF]
• Fred B. Schneider. Enforceable Security Policies. ACM Transactions on Information and System Security 3, 1 (Feb. 2000), 30-50. 
• Ulfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: A retrospective. Proceedings of the New Security Paradigm Workshop (Caledon Hills, Ontario, Canada, September 22-24, 1999), Association for Computing Machinery, 1515 Broadway, NY, NY, 87-95.
• Ulfar Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. Proceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), IEEE Computer Society, Los Alamitos,California, 246-255.
• David Walker. A type system for expressive security properties.  In the Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254-267, Boston, MA, USA, January 2000.

Typed Assembly Language and Type-Safe C:

• Michael Hicks, Greg Morrisett, Dan Grossman and Trevor Jim.  Experience with Safe Manual Memory Management in Cyclone.  In ACM International Symposium on Memory Management, October 2004.
• Matthew Fluet and Greg Morrisett.  Monadic Regions.  In ACM International Conference on Functional Programming, September 2004.
• Mike Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim.  Safe and Flexible Memory Management in Cyclone.  University of Maryland Technical Report CS-TR-4514, July 2003.
• Greg Morrisett.  Type-Checking Systems Code.  European Symposium on Programming, Grenoble, France, April 2002.  
• Karl Crary, Stephanie Weirich, and Greg Morrisett.  Intensional Polymorphism in Type Erasure Semantics.  Journal of Functional Programming, To appear.
• Trevor Jim, Greg Morrisett, Dan Grossman, Mike Hicks, James Cheney and Yanling Wang. Cyclone:  A Safe Dialect of C.  Usenix Annual Technical Conference, pages 275-288, Monterey, CA, June 2002.
• Dan Grossman, Greg Morrisett, Trevor Jim, Mike Hicks, James Cheney and Yanling Wang.  Region-Based Memory Management in Cyclone.  ACM Conference on Programming Language Design and Implementation, page 282-293, Berlin, Germany, June 2002. 
• Fred Smith, Dan Grossman, Greg Morrisett, Luke Hornoff, and Trevor Jim.  Compiling for Template-Based Runtime Code Generation.  Journal of Functional Programming, 13(3):677-708, May 2003.
• James Cheney and Greg Morrisett.  A Linearly-Typed Assembly Language.  Cornell Technical Report, February 2003.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew.  From System F to Typed Assembly Language.  In ACM Transactions on Programming Languages and Systems, 21(3):528-569, May 1999.
• Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language.  In the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, Atlanta, GA, USA, May 1999.
• Neal Glew and Greg Morrisett.  Type-safe linking and modular assembly language.  In the Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 250-261, San Antonio, TX, USA, January 1999.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In the 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer-Verlag, 1998.
• Greg Morrisett and Karl Crary.  Type structure for low-level programming languages.  In 1999 International Colloquium on Automata, Languages, and Programming. 

Type-Based Information Flow Enforcement:

• Lantian Zheng, Andrew C. Myers. End-to-End Availability Policies and Noninterference Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), June 2005.
• Belief in Information Flow.  Proceedings 18th IEEE Computer Security Foundations Workshop (Aux-en-Provence, France, June 20-22, 2005), 31--45.  Earlier version  available as Cornell Computer Science Department Technical Report TR 2005-1976, February 2005. With Michael R. Clarkson and Andrew C. Myers.
• Belief in Information Flow Michael Clarkson, Andrew C. Myers, Fred B. Schneider. Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), June 2005.
• Stephen Chong, Andrew C. Myers. Language-Based Information Erasure Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), June 2005.
• Stephen Chong, Andrew C. Myers. Security Policies for Downgrading. To appear in 11th ACM Conference on Computer and Communications Security, Washington, DC, October 2004.
• Stephen Chong, Andrew C. Myers. Security Policies for Downgrading  Proceedings of the 11^th ACM Conference on Computer and Communications Security (CCS), pages 189–209, Washington, DC, USA, October 2004.
• Lantian Zheng and Andrew C. Myers. Dynamic Security Labels and Noninterference. To appear in Workshop on Formal Aspects in Security and Trust (FAST), Toulouse, France, August 2004.
• Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing Robust Declassification. Proceedings of the 17th IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2004, pages 172-186.
• Andrei Sabelfeld and Andrew C. Myers. A Model for Delimited Release. To appear in Proceedings of the 2003 International Symposium on Software Security. LNCS, Springer-Verlag, 2004.
• Steve Zdancewic, Andrew C. Myers. Observational Determinism for Concurrent Program Security. Proceedings of the 16th IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2003, pages 29–43.
• Lantian Zheng, Stephen Chong, Andrew C. Myers, Steve Zdancewic. Using Replication and Partitioning to Build Secure Distributed Systems. Proceedings of the 2003 IEEE Symposium on Security and Privacy, Oakland, California, May 2003, pages 236–250.
• Andrei Sabelfeld, Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communication, special issue on Formal Methods for Security, 21(1), January 2003, pages 5-19.
• Steve Zdancewic, Andrew C. Myers. Secure information flow and linear continuations. Higher Order and Symbolic Computation, 15(2-3), September 2002, pages 209-234.
• Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers.  Untrusted hosts and confidentiality: secure program partitioning  Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), Banff, Canada, October 2001, pages 1-14. Award Paper.
• Steve Zdancewic, Andrew C. Myers.  Robust declassification. Proceedings of the 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, June 2001, pages 15-23.
• Steve Zdancewic, Andrew C. Myers.  Secure information flow and CPS.  Proceedings of the 10th European Symposium on Programming, Genova, Italy, April 2001, pages 46-61.
• Andrew C. Myers, Barbara Liskov.  Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology, 9(4), October 2000, pages 410-442.
• Andrew C. Myers.  JFlow: Practical mostly-static information flow control.  Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, January 1999, pages 228-241.
• Andrew C. Myers, Barbara Liskov.  Complete, safe information flow with decentralized labels.
  Proceedings of the 1998 IEEE Symposium on Security and Privacy, Oakland, California, May 1998, pages 186-197. 
• Andrew C. Myers, Barbara Liskov.  A decentralized model for information flow control.  Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP), Saint-Malo, France, October 1997, pages 129-142.

Efficient Code Certification:

• Dexter Kozen.  "Efficient code certification," Tech. Report 98-1661, Cornell Univ., January 1998. 
• Dan Grossman and Greg Morrisett.  Scalable certification for Typed Assembly Language.  In the 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000.
• Frank Adelstein, Dexter Kozen and Matt Stillerman. Malicious Code Detection for Open Firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), Las Vegas, December 2002, pages 403-412.

Misc:

• Dexter Kozen. On the representation of Kleene algebras with tests. Technical Report 2003-1910, Computer Science Department, Cornell University, September 2003.
•  Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. In Boris Konev and Renate Schmidt, editors, Proc. 4th Int. Workshop on the Implementation of Logics (WIL'03), 2-12. University of Manchester, September 2003.
• Chris Hardin and Dexter Kozen. On the Complexity of the Horn Theory of REL. Technical Report 2003-1896, Computer Science Department, Cornell University, May 2003.
• Dexter Kozen. Some Results in Dynamic Model Theory. Technical Report 2002-1882, Computer Science Department, Cornell University, October 2002.
• Dexter Kozen. Halting and Equivalence of Schemes over Recursive Theories. Technical Report 2002-1881, Computer Science Department, Cornell University, October 2002.
• Chris Hardin and Dexter Kozen. On the Elimination of Hypotheses in Kleene Algebra with Tests. Technical Report 2002-1879, Computer Science Department, Cornell University, October 2002.
• Adam Barth and Dexter Kozen. Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests. Technical Report 2002-1865, Computer Science Department, Cornell University, June 2002.
• Dexter Kozen. Computational Inductive Definability. Technical Report 2002-1870, Computer Science Department, Cornell University, April 2002.
• Allegra Angus and Dexter Kozen. Kleene Algebra with Tests and Program Schematology. Technical Report 2001-1844, Computer Science Department, Cornell University, July 2001.
• Dexter Kozen and Jerzy Tiuryn. Substructural Logic and Partial Correctness. Trans. Computational Logic, 4(3), July 2003, 355-378.
• Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139 (2001), 187-195.
• Dexter Kozen. On Hoare Logic, Kleene Algebra, and Types. In P. Gärdenfors, J. Wolenski, and K. Kijania-Placek, editors, In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999, volume 315 of Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 119-133. Kluwer, 2002.
• Dexter Kozen. On the Complexity of Reasoning in Kleene Algebra. Information and Computation 179, 152-162, 2002.
• Dexter Kozen and Matt Stillerman. Eager Class Initialization for Java. In W. Damm and E.R. Olderog, editors, Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 71-80. IFIP, Springer-Verlag, Sept. 2002.
• Robert Givan, David McAllester, Carl Witty and Dexter Kozen. Tarskian Set Constraints. Information and Computation, 174(2):105-131, May 2002.
• Dexter Kozen. On Two Letters versus Three. Technical Report 2002-1860, Computer Science Department, Cornell University, February 2002.
• Dexter Kozen. Automata on Guarded Strings and Applications. Matématica Contemporânea 24 (2003), 117-139.
• Stanislaw M. Dziobiak. A comparison of eager and lazy class initialization in Java. Technical Report 2003-1911, Computer and Information Science, Cornell University, September 2003.