CS 297, CS 197: Security and Programming Languages

Papers

• Overview:
  • 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.
  • R.Simha, A.Choudhary, B.Narahari and J.Zambreno. An Overview of Security-Driven Compilation. Workshop on New Horizons in Compiler Analysis, 2004.
  • McGraw, Gary and Greg Morrisett. Attacking Malicious Code. In IEEE Software, Volume 17(5), September/October 2000.
  • Fred B. Schneider. Enforceable Security Policies. ACM Transactions on Information and System Security 3, 1 (Feb. 2000), 30-50.
  • Crispin Cowan. Software Security for Open Source Systems. IEEE Security & Privacy Magazine, February 2003, Volume 1, Number 1, pages 35-48.
  • RS BOYER, JS MOORE. Proof-checking, theorem proving and program verification.

• Group A: C and Java
  1. 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.
  2. G.Necula et al. Taming C Pointers.
  3. George C. Necula, Jeremy Condit, Matthew Harren. CCured: Type-Safe Retrofitting of Legacy Software. ACM Transactions on Programming Languages and Systems (TOPLAS), to appear, 2004.
  4. D.Wheeler. Java Security Overview
  5. Aspect oriented programing and AspectJ. Example: R.Pewlak et al. JAC: An Aspect Based Distributed Dynamic Framework.
  6. Sunil Soman, Chandra Krintz, and Giovanni Vigna. Detecting Malicious Java Code Using Virtual Machine Auditing. 12th USENIX Security Symposium, Washington DC, Aug. 4-8, 2003.
  7. 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.

• Group B: Certifying compilers
  1. GC Necula, P Lee. The Design and Implementation of a Certifying Compiler PLDI, 1998.
  2. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Ken Cline, Mark Plesko. A Certifying Compiler for Java, Conference on Programming Language Design and Implementation (PLDI00), Vancouver, British Columbia, Canada, June 18-21, 2000.

• Group C: Strong Typing
  1. 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.
  2. Kedar N. Swadi and Andrew W. Appel. Typed Machine Language and its Semantics.
  3. 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.

• Group D: Proof-Carrying Code
  1. George C. Necula. Proof-Carrying Code . POPL97, January 1997.
  2. Andrew W. Appel and Edward W. Felten. Proof-Carrying Authentication. 6th ACM Conference on Computer and Communications Security, November 1999.

• Group E: Rule checking
  1. George C. Necula, Peter Lee. Safe Kernel Extensions Without Run-Time Checking. OSDI'96,October 1996.
  2. H.Chen and J.S.Shapiro. Using build-integrated static checking to preserve correctness invariants. Proceedings of the 11th ACM conference on Computer and communications security, Washington DC, 2004.
  3. Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. OSDI 2000.
  4. Madanlal Musuvathi, David Y.W. Park, Andy Chou, Dawson R. Engler, David L. Dill. CMC: A pragmatic approach to model checking real code. ISCA 2001.
  5. Junfeng Yang, Ted Kremenek, Yichen Xie, and Dawson Engler. MECA: an Extensible, Expressive System and Language for Statically Checking Security Properties. ACM CCS, 2003.
  6. Dawson Engler and Ken Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. SOSP 2003.
  7. Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, and Benjamin Chelf. Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code. OSDI 2000.
  8. Christian S. Collberg, Todd A. Proebsting. Problem Classification using Program Checking.
  9. E.Larson, T.Austin. High Coverage Detection of Input-Related Security Faults. 12th Usenix Security Symposium, 2003.
  10. J Crow, S Owre, J Rushby, N Shankar, M Srivas. A Tutorial Introduction to PVS.

• Group F: Watermarking and digests
  1. Mikhail J. Atallah. A Survey of Watermarking Techniques for Non-Media Digital Objects. ACSW Frontiers 2005: 73.
  2. Hoi Chang, Mikhail J. Atallah. Protecting Software Code by Guards. Digital Rights Management Workshop 2001: 160-175.
  3. Christian S. Collberg , Clark Thomborson. Software Watermarking: Models and Dynamic Embeddings. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL99), San Antonio, Texas

• Group G: Stacks and Buffer-overflow
  1. Crispin Cowan, Calton Pu, Dave Maier, Heather Hinton, Peat Bakke, Steve Beattie, Aaron Grier, Perry Wagle, and Qian Zhang. StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks. 7th USENIX Security Symposium, January 1998, San Antonio, TX.
  2. Crispin Cowan, Perry Wagle, Calton Pu, Steve Beattie, and Jonathan Walpole. Buffer Overflows: Attacks and Defenses for the Vulnerability of the Decade . SANS 2000, Orlando FL, March 2000.
  3. K.S.Hlee and J.S.Chapin. Type-Assisted Dynamic Buffer Overflow Detection. 11th Annual USENIX Security Symposium.

• Group H: Hardware and OS
  1. Chris Wright, Crispin Cowan, Stephen Smalley, James Morris, and Greg Kroah-Hartman. Linux Security Module Framework. 2002 Ottawa Linux Symposium, Ottawa, Canada, June 2002.
  2. Chris Wright, Crispin Cowan, Stephen Smalley, James Morris, and Greg Kroah-Hartman. Linux Security Modules: General Security Support for the Linux Kernel. 11th USENIX Security Symposium, San Francisco, CA, August 2002.
  3. An example of using LSM, e.g., Domain and Type Enforcement for Linux.
  4. Kenneth M. Walker, Daniel F. Sterne, M. Lee Badger,Michael J. Petkac, David L. Shermann. Confining Root Programs with Domain and Type Enforcement. Proceedings of the 6th Usenix Security Symposium, San Jose, California, 1996.
  5. Rob Johnson and David Wagner. Finding User/Kernel Pointer Bugs With Type Inference. (Postscript) USENIX Security Symposium, 2004.
  6. W. A. Arbaugh, D. J. Farber, and J. M. Smith. A Secure and Reliable Bootstrap Architecture. IEEE Symposium on Security and Privacy , pp. 65-71, May 1997.
  7. David Brumley and Dawn Song. Privtrans: Automatic Privilege Separation. USENIX Security Symposium 2004.
  8. S.Smith. Magic Boxes and Boots: Security in Hardware. IEEE Computer. 37 (10): 106--109. October 2004.
  9. S.W. Smith, D. Safford. Practical Server Privacy Using Secure Coprocessors. IBM Systems Journal 40: 683-695. 2001.
  10. S.W. Smith. Secure Coprocessing Applications and Research Issues. Los Alamos Unclassified Release LA-UR-96-2805, Los Alamos National Laboratory.
  11. Xiaotong Zhuang, Tao Zhang, Hsien-Hsin Lee and Santosh Pande. Hardware Assisted Control Flow Obfuscation for Embedded Processors. CASES, Washington DC, Sept. 2004.
  12. Zhuang, X., Zhang, T. and Pande, S. HIDE: An Infrastructure for Efficiently Protecting Information Leakage on the Address Bus. International Conference on Architectural Support for Programming Languages and Operating Systems, Boston, MA., Oct 2004.
  13. D Lie, CA Thekkath, M Mitchell, P Lincoln, D Boneh. Architectural Support for Copy and Tamper Resistant Software.
  14. J.Zambreno, A.Choudhary, B.Narahari, R.Simha and N.Memon. SAFE-OPS: A Compiler/Architecture Approach to Embedded Software Security . ACM Trans. Embedded Computing, Vol. 4, No. 1, Feb 2005.

• Group I: Miscellaneous
  1. 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.
  2. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre. Lazy Abstraction. ACM Symposium on Principles of Programming Languages (POPL 2002).
  3. P.Wilson et al. Dynamic Storage Allocation: A Survey and Critical Review. Int. Workshop on Memory Management, 1995. See also P.Wilson's tutorial: Uniprocessor Garbage Collection Techniques.
  4. David Gay and Alex Aiken. Language Support for Regions. ACM SIGPLAN '01 Conference on Programming Language Design and Implementation, Snowbird, Utah, June 2001.
  5. Papers on Worms. See the two papers under the 4/26 listing at http://www.cs.ucdavis.edu/~hchen/teaching/malware-s05/
  6. C.R.Gould, Z.Su and P.Devanbu. Static Checking of Dynamically Generated Queries in Database Applications. ICSE 2004, Edinburgh, UK.
  7. P.H.Runge Software Verification Tools
  8. H.Shacham et al. On the effectiveness of address-space randomization. Proceedings of the 11th ACM conference on Computer and communications security, Washington DC, 2004.