CS-342: Security and Programming Languages

Papers

• Overview:
  • An Overview of Security-Driven Compilation. Workshop on New Horizons in Compiler Analysis, 2004.
  • C.Cowan. Software Security for Open Source Systems. IEEE Security & Privacy Magazine, February 2003, Volume 1, Number 1, pages 35-48.
  • R.S.Boyer and J.S.Moore. Proof-checking, theorem proving and program verification.
  • C.S.Collberg and C.Thomborson. Software Watermarking: Models and Dynamic Embeddings. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL99), San Antonio, Texas
  • F.B.Schneider, G.Morrisett and R.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 A1: Languages (C-based)
  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.Fandrich. The Vault programming language

• Group A2: Languages (C-based)
  1. G.C.Necula, J.Condit, M.Harren. CCured: Type-Safe Retrofitting of Legacy Software. ACM Transactions on Programming Languages and Systems (TOPLAS), 2004.
  2. CQUAL: A Tool for adding type qualifiers to C

• Group A3: Languages (Java)
  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. S.Soman, C.Krintz and G.Vigna. Detecting Malicious Java Code Using Virtual Machine Auditing. 12th USENIX Security Symposium, Washington DC, Aug. 4-8, 2003.

• Group A4: Languages - Type-safe assembly
  1. G.Morrisett, K.Crary, N.Glew, D.Grossman, R.Samuels, F.Smith, D.Walker, S.Weirich and S.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. K.N.Swadi and A.W.Appel. Typed Machine Language and its Semantics.

• Group B1: Rule checking
  1. D.Engler, B.Chelf, A.Chou, and S.Hallem. Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. OSDI 2000.
  2. D.Engler, D.Chen, S.Hallem, A.Chou and B.Chelf. Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code. OSDI 2000.
  3. D.Engler and K.Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. SOSP 2003.

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

• Group C2: Runtime systems and languages
  1. G.Hunt et al. An Overview of the Singularity Project (Microsoft)
  2. Microsoft's F# project.

• Group D: 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.

• Group E1: Transactional memory
  1. M.Herlihy. The Transactional Manifesto: Software Engineering and Non-blocking Synchronization.
  2. M.Herlihy and J.E.B.Moss. Transactional Memory: Architectural Support for Lock-Free Data Structures , ISCA 1993.
  3. Y.Ni and A.Welc. Transactional Memory: From Semantics to Implementation.

• Group E2: Transactional memory
  1. B.Carlstrom et al. The Atomos Trans programming language, PLDI 2006. See also slides
  2. B.Carlstrom et al. Executing Java Programs with Transactional Memory, 2007.

• Group E3: Transactional memory
  1. Y.Ni, V.Menon, A.Adl-Tabatabai, A.L.Hosking, R.L.Hudson, J.E.B.Moss, B.Saha, T.Shpeisman. Open Nesting in Software Transactional Memory , ACM SIGPLAN 2007.
  2. K.E.Moore, J.Bobba, M.J.Moravan, M.D.Hill and D.Wood. LogTM: Log-based Transactional Memory, Symposium on High Performance Computer Architecture (HPCA), February 2006.

• Group F: Virtualization
  1. T.Garfinkel and A.Warfield. What Virtualization can do for Security , USENIX Magazine, December 2007.
  2. X.Chen, T.Garfinkel, E.Lewis, P.Subrahmanyam, C.A.Waldspurger, D.Boneh, J.Dwoskin, D.Ports. Overshadow: A Virtualization-Based Approach to Retrofitting Protection in Commodity Operating Systems, ASPLOS 2008.

• Group G1: Real-time
  1. E.Lee. The Problem with Threads.
  2. E.Lee. Cyber Physical Systems: Design Challenges International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), May, 2008.
  3. P.Derler, T.H.Feng, E.A.Lee, S.Matic, H.D.Patel, Y.Zhao and J.Zou, PTIDES: A Programming Model for Distributed Real-Time Embedded Systems , EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2008-72, May 2008.

• Group G2: Real-time
  1. F.Boussinot. Java Fair Threads.
  2. G.Berry and G.Gonthier. The Esterel Synchronous Programming Language
  3. M.Riesco and J.Tuya. Synchronous Estelle: Just Another Synchronous Language?

• Group G3: Real-time
  1. G.Wang and P.Cook. Chuck: A Strongly-timed, Concurrent, and On-the-fly Audio Programming Language.
  2. Europa.

• Group H: Audit
  1. J.A.Vaughan, L.Jia, K.Mazurak and S.Zdancewic. Evidence-based Audit , IEEE Computer Security Foundations Symposium (CSF), pages 177-191, 2008.
  2. L.Jia, J.Vaughan, K.Mazurak, J.Zhao, L.Zarko, J.Schorr and S.Zdancewic. AURA: A Programming Language for Authorization and Audit, in SIGPLAN International Conference on Functional Programming (ICFP), British Columbia, Canada, September 2008.

• Group I: Aspects
  1. G.Kiczales et al. AspectJ.
  2. G.Washburn and S.Weirich. Good Advice for Type-directed Programming: Aspect-oriented Programming and Extensible Generic Functions

• Group J1: OOP
  1. 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.
  2. J.M.Chang et al. Architectural support for dynamic memory management, Conf. Computer Design, 2000.
  3. M.Meyer. An On-Chip Garbage Collection Coprocessor for Embedded Real-Time Systems, IEEE Int. Conf. Embedded and Real-Time Computing Systems and Applications, 2005.

• Group J2: OOP
  1. U.Holzle and D.Ungar. Do object-oriented languages need special hardware support? ECOOP 1995.
  2. J.Kaiser and K.Czaja. Lightweight Hardware Support for Protection in OO Systems, 1992.
  3. I.Williams and M.Wolczko. An Object-Based Memory Architecture, Workshop on Persistent Object Systems, 1991.

• Group K1: Policy
  1. Policy languages: A review, W3C.
  2. N.Damianou et al. A Survey of Policy Specification Approaches
  3. P.Kumaraguru et al. A Survey of Privacy Policy Languages

• Group K2: RBAC
  1. D.F. Ferraiolo and D.R. Kuhn. Role Based Access Control, 15th National Computer Security Conference, Oct 13-16, 1992, pp. 554-563.
  2. R.S.Sandhu, E.J.Coyne, H.L.Feinstein, C.E.Youman (1996), Role-Based Access Control Models IEEE Computer 29(2): 38-47, 1996.
  3. M.Hitchens and V.Varadharajan. Tower: A language for role based access control.
  4. T.Finin, A.Joshi, L.Kagal, J.Niu, R.Sandhu, W.Winsborough and B.Thuraisingham. ROWLBAC: Representing Role Based Access Control in OWL, Proc. 13th ACM Symposium on Access Control Models and Technologies (SACMAT), Estes Park, Colorado, June 11-13, 2008, pages 73-82.

• Group K3: RBAC
  1. R.Sandhu and J.Park. Usage Control: A Vision for Next Generation Access Control, MMM-ACNS 2003.
  2. R.Sandhu and V.Bhamidipati. The ASCAA Principles for Next-Generation Role-Based Access Control. Proc. 3rd International Conference on Availability, Reliability and Security (ARES), Barcelona, Spain, March 4-7, 2008.
  3. M.Xu, X.Jiang, R.Sandhu and X.Zhang. Towards a VMM-based Usage Control Framework for OS Kernel Integrity Protection. Proc. 12th ACM Symposium on Access Control Models and Technologies (SACMAT), June 20-22, 2007, Sophia Antipolis, France, pages 71-80.

• Group L: Recovery
  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. D.A. de Oliveira, J.R.Crandall, G.Wassermann, F.Wu, Z.Su, and F.Chong. ExecRecorder: VM-based full-system replay for attack analysis and system recovery. 1st Workshop on Architectural and System Support For Improving Software Dependability (San Jose, California, October 21 - 21, 2006). ASID '06.
  3. D.Lowell and P.Chen. Discount Checking: Transparent, Low-Overhead Recovery for General Applications. Technical Report CSE-TR-410-99, University of Michigan, 1998
  
  
  
  

• Miscellaneous
  1. G.C.Necula. Proof-Carrying Code. POPL97, January 1997.
  2. G.C.Necula and P.Lee. The Design and Implementation of a Certifying Compiler PLDI, 1998.
  3. V.Kiriansky, D.Bruening and S.Amarasinghe. Secure Execution Via Program Shepherding USENIX Security Symposium, 2002.
  4. 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.
  5. Aspect oriented programing and AspectJ. Example: R.Pewlak et al. JAC: An Aspect Based Distributed Dynamic Framework.
  6. 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.
  7. 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.
  8. G.C.Necula, P.Lee. Safe Kernel Extensions Without Run-Time Checking. OSDI'96,October 1996.
  9. 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.
  10. 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.
  11. J.Yang, T.Kremenek, Y.Xie and D.Engler. MECA: an Extensible, Expressive System and Language for Statically Checking Security Properties. ACM CCS, 2003.
  12. C.S.Collberg, T.Proebsting. Problem Classification using Program Checking.
  13. E.Larson, T.Austin. High Coverage Detection of Input-Related Security Faults. 12th Usenix Security Symposium, 2003.
  14. J Crow, S Owre, J Rushby, N Shankar, M Srivas. A Tutorial Introduction to PVS.
  15. K.S.Hlee and J.S.Chapin. Type-Assisted Dynamic Buffer Overflow Detection. 11th Annual USENIX Security Symposium.
  16. R.Johnson and D.Wagner. Finding User/Kernel Pointer Bugs With Type Inference. (Postscript) USENIX Security Symposium, 2004.
  17. 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.
  18. D.Brumley and D.Song. Privtrans: Automatic Privilege Separation. USENIX Security Symposium 2004.
  19. S.W.Smith, D.Safford. Practical Server Privacy Using Secure Coprocessors. IBM Systems Journal 40: 683-695. 2001.
  20. S.W.Smith. Secure Coprocessing Applications and Research Issues. Los Alamos Unclassified Release LA-UR-96-2805, Los Alamos National Laboratory.
  21. D.Gay and A.Aiken. Language Support for Regions. ACM SIGPLAN '01 Conference on Programming Language Design and Implementation, Snowbird, Utah, June 2001.
  22. Papers on Worms. See the two papers under the 4/26 listing at http://www.cs.ucdavis.edu/~hchen/teaching/malware-s05/
  23. C.R.Gould, Z.Su and P.Devanbu. Static Checking of Dynamically Generated Queries in Database Applications. ICSE 2004, Edinburgh, UK.
  24. P.H.Runge Software Verification Tools
  25. 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.
  26. M.Gaiman, R.Simha and B.Narahari. Privacy-Preserving Programming Using Sython. J. Computers and Security, to appear.
  27. 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.
  28. Xiaotong Zhuang, Tao Zhang, Hsien-Hsin Lee and Santosh Pande. Hardware Assisted Control Flow Obfuscation for Embedded Processors. CASES, Washington DC, Sept. 2004.