CS-342: Security and Programming Languages

Papers

• Overview:
  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.
  • D.Wheeler. Java Security Overview
  • Mikhail J. Atallah. A Survey of Watermarking Techniques for Non-Media Digital Objects. ACSW Frontiers 2005: 73.
  • 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 A1: C-Based Tools
  1. T.Jim, G.Morrisett, D.Grossman, M.Hicks, J.Cheney and Y.Wang. Cyclone: A Safe Dialect of C. Usenix Annual Technical Conference, pages 275-288, Monterey, CA, June 2002.
  2. R.DeLine and M.Fahnrich. Vault: A Programming Language for Reliable Systems.

• Group A2: C-Based Tools
  1. G.Necula et al. Taming C Pointers.
  2. 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.
  3. CQUAL: A Tool for adding type qualifiers to C

• Group A3: Java-Based Tools
  1. C.Flanagan, K.R.M.Leino, K.Lillibridge, G.Nelson, J.B.Saxe and R.Stata. Extended Static Checking for Java
  2. Java Pathfinder project
  3. 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.

• Group B1: 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.
  3. GC Necula, P Lee. The Design and Implementation of a Certifying Compiler PLDI, 1998.
  4. 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 B2: Type-safe assembly
  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.

• Group B3: Rule checking
  1. Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. OSDI 2000.
  2. Dawson Engler and Ken Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. SOSP 2003.
  3. 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.

• Group B4: Rule checking
  1. SLAM project at Microsoft
  2. T.Ball and S.K.Rajamani. Checking Temporal Properties of Software with Boolean Programs. Workshop on Advances in Verification (with CAV 2000)

• Group C1: Runtime systems
  1. V.Kiriansky, D.Bruening and S.Amarasinghe. Secure Execution Via Program Shepherding USENIX Security Symposium, 2002.
  2. S.Zdancewic, L.Zheng, N.Nystrom and A.C.Myers. Secure Program Partitioning ACM Transactions on Computer Systems (TOCS), Vol.20, No.3, August 2002.

• Group C2: Runtime systems
  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. M.Kharbutli, X.Jiang, Y.Solihin, G.Venkataramani and M.Prvulovic. Comprehensively and Efficiently Protecting the Heap. ASPLOS 2006.

• Group C3: Runtime systems
  1. Hoi Chang, Mikhail J. Atallah. Protecting Software Code by Guards. Digital Rights Management Workshop 2001: 160-175.
  2. 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 C4: Runtime systems
  1. G.Candea, S.Kawamoto, Y.Fujiki, G.Friedman, A.Fox Microreboot - A Technique for Cheap Recovery. 6th Symposium on Operating Systems Design and Implementation (OSDI), San Francisco, CA, December 2004
  2. G.Candea and A.Fox Crash-Only Software. 9th Workshop on Hot Topics in Operating Systems (HotOS), Lihue, Hawaii, May 2003
  3. G.Candea and A.Fox. Recursive Restartability: Turning the Reboot Sledgehammer into a Scalpel. 8th Workshop on Hot Topics in Operating Systems (HotOS), Schloss Elmau, Germany, May 2001
  4. D.Patterson, A.Brown, P.Broadwell, G.Candea, M.Chen, J.Cutler, P.Enriquez, A.Fox, E.Kiciman, M.Merzbacher, D.Oppenheimer, N.Sastry, W.Tetzlaff, N.Treuhaft, Recovery Oriented Computing (ROC): Motivation, Definition, Techniques, and Case Studies. UC Berkeley Computer Science Technical Report UCB/CSD-02-1175, March 15, 2002

• Group D: Components
  1. K-K.Lau and Z.Wang. A Survey of Software Component Models. Pre-print CSPP-38, School of Computer Science, The University of Manchester, May 2006.
  2. N.Nystrom, X.Qi, A.C.Myers. J&: Nested Intersection for Scalable Software Composition. OOPLSA, October 2006.
  3. Y.Cheon and G.Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. Euro Conf. on OOP, 2002, Malaga, Spain.

• Group E: Embedded systems
  1. A.Seshadri, A.Perrig, L.Van Doorn and P.Khosla. Software-Based Attestation for Embedded Devices. 2004 IEEE Symposium on Security and Privacy.
  2. A.Seshadri, A.Perrig, L.van Doorn and P.Khosla. Using SWATT for Verifying Embedded Systems in Cars. 2004 Embedded Security in Cars Workshop.
  3. L.de Alfaro and T.Henzinger. Interface Automata Proc. Foundations of Software Engineering (FSE), ACM Press, 2001, pp. 109-120. See project website

• Group F: Information Flow
  1. A.C.Myers and B.Liskov. Protecting Privacy using the Decentralized Label Model. ACM Transactions on Software Engineering and Methodology, 9(4):410-442, October 2000.
  2. S.Chong and A.C.Myers. Decentralized Robustness. Proc. Computer Security Foundations Workshop (CSFW'06), pages 242-253, July 2006.
  3. 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.
  4. 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.

• Group G1: Hardware support
  1. E.Witchel, J.Cates and K.Asanovic. Mondrian Memory Protection. ASPLOS, San Jose, CA, October 2002.
  2. W.Shi, J.B.Fryman, G.Gu, H.H.S.Lee, Y.Zhang and J.Yang. Infoshield: A Security Architecture for Protecting Information Usage in Memory. HPCA 2006.
  3. J.Yang, L.Gao and Y.Zhang, Improving Memory Encryption Performance in Secure Processors. IEEE Transactions on Computers, pp. 630-640, Vol. 54, No. 5, May 2005.

• Group G2: Hardware support
  1. B.Kuperman, C.Brodley, H.Ozdoganoglu, T.N.Vijaykumar and A.Jalote. Detection and Prevention of Stack Buffer Overflow Attacks
  2. 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.
  3. Xiaotong Zhuang, Tao Zhang, Hsien-Hsin Lee and Santosh Pande. Hardware Assisted Control Flow Obfuscation for Embedded Processors. CASES, Washington DC, Sept. 2004.

• Group G3: Hardware support
  1. S.Smith. Magic Boxes and Boots: Security in Hardware. IEEE Computer. 37 (10): 106--109. October 2004.
  2. D Lie, CA Thekkath, M Mitchell, P Lincoln, D Boneh. Architectural Support for Copy and Tamper Resistant Software.

• Group H: Operating systems
  1. M.Swift, B.Bershad and H.Levy. Improving the Reliability of Commodity Operating Systems<. ACM Transactions on Computer Systems, 22(4), Nov. 2004.
  2. C..Wright, C.Cowan, S.Smalley, J.Morris and G.Kroah-Hartman. Linux Security Module Framework. 2002 Ottawa Linux Symposium, Ottawa, Canada, June 2002.
  3. C.Wright, C.Cowan, S.Smalley J.Morris and G.Kroah-Hartman. Linux Security Modules: General Security Support for the Linux Kernel. 11th USENIX Security Symposium, San Francisco, CA, August 2002.
  4. K.M.Walker, D.F.Sterne, M.Lee Badger, M.J.Petkac, D.L.Shermann. Confining Root Programs with Domain and Type Enforcement. Proceedings of the 6th Usenix Security Symposium, San Jose, California, 1996.

• Miscellaneous
  1. Aspect oriented programing and AspectJ. Example: R.Pewlak et al. JAC: An Aspect Based Distributed Dynamic Framework.
  2. U.Erlingsson and F.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.
  3. D.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.
  4. G.C.Necula, P.Lee. Safe Kernel Extensions Without Run-Time Checking. OSDI'96,October 1996.
  5. 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.
  6. M.Musuvathi, D.Y.W. Park, A.Chou, D.R.Engler and D.L.Dill. CMC: A pragmatic approach to model checking real code. ISCA 2001.
  7. J.Yang, T.Kremenek, Y.Xie and D.Engler. MECA: an Extensible, Expressive System and Language for Statically Checking Security Properties. ACM CCS, 2003.
  8. C.S.Collberg, T.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.
  11. K.S.Hlee and J.S.Chapin. Type-Assisted Dynamic Buffer Overflow Detection. 11th Annual USENIX Security Symposium.
  12. R.Johnson and D.Wagner. Finding User/Kernel Pointer Bugs With Type Inference. (Postscript) USENIX Security Symposium, 2004.
  13. 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.
  14. D.Brumley and D.Song. Privtrans: Automatic Privilege Separation. USENIX Security Symposium 2004.
  15. S.W.Smith, D.Safford. Practical Server Privacy Using Secure Coprocessors. IBM Systems Journal 40: 683-695. 2001.
  16. S.W.Smith. Secure Coprocessing Applications and Research Issues. Los Alamos Unclassified Release LA-UR-96-2805, Los Alamos National Laboratory.
  17. 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.
  18. D.Gay and A.Aiken. Language Support for Regions. ACM SIGPLAN '01 Conference on Programming Language Design and Implementation, Snowbird, Utah, June 2001.
  19. Papers on Worms. See the two papers under the 4/26 listing at http://www.cs.ucdavis.edu/~hchen/teaching/malware-s05/
  20. C.R.Gould, Z.Su and P.Devanbu. Static Checking of Dynamically Generated Queries in Database Applications. ICSE 2004, Edinburgh, UK.
  21. P.H.Runge Software Verification Tools
  22. 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.
  23. M.Gaiman, R.Simha and B.Narahari. Privacy-Preserving Programming Using Sython. J. Computers and Security, to appear.