CS 528, Spring 2009, Course Information

CS 528 Course Information, Spring 2009

Last modified: January 14, 2009.

Content

General Information

Language-Based Security (LBS) is a promising new research area, aimed toward ``completely'' eliminating specific classes of vulnerabilities introduced by the semantics of programing languages and higher-level library interfaces. Programming language technologies, including type systems, proof systems, static analyses, interpreters, rewriters, and compilers are the key components of next generation security systems. This course will present a survey of the most promising LBS techniques and show how to apply these techniques in building high-confidence embedded system software.

Title:
CS528: Language-Based Security (Spring 2009)

Lectures:
MW 1:00 PM-2:15 PM, in 200 AKW

Instructor:
Zhong Shao, 314 Watson, 432-6828, shao at cs dot yale dot edu
Office hours (for class): MW 4:00 PM - 5:00 PM or by appt.

Teaching Assistant:
Alex Vaynberg, 312 Watson, office: 432-2349, cell: (804)519-2540 alv at cs dot yale dot edu
Office hours: TBA or by appt.

Main Topics

  • Motivation and Overview

  • Target applications (software)
  • OS kernels (Singularity, L4, HiStar/DStar/Loki, Flume, OSKit, JKernel)
  • Hypervisors and VMM
  • Device drivers
  • Web applications (JavaScript, mashups, GWT, Json)
  • Voting systems
  • C compiler
  • Software for Cyber-Physical Systems (embedded systems, medical devices)

  • Specification languages
  • Propositional vs predicate logic
  • Meta logic vs object logic vs domain-specific logics
  • Inductive definitions
  • Hoare assertions, UML, VDM, and Z
  • Proof assistants (Coq, HOL, Twelf)
  • Type systems
  • Programming language syntax and semantics

  • Enforcement mechanisms
  • How to write good specifications and dependability claims
  • Mechanized proof objects and Curry-Howard isomorphism
  • Automated program verifiers and theorem provers (Boogie, Z3, VCC)
  • Proof engineering (how to write proofs)
  • Model checking tools

  • Language-based technologies
  • Hoare-style program verification
  • Formal semantics and type systems
  • Certified assembly programming
  • Proof-carrying code and typed assembly language
  • Separation logic and concurrent separation logic
  • Decentralized information flow control
  • Security-typed programming language (Jif)
  • Concurrency and rely-guarantee reasoning
  • The SPARK approach (Praxis Critical Systems)
  • Techniques for enforcing mashup security
  • Techniques for proving liveness property
  • Techniques for certifying interrupt handlers and device drivers

    • Textbooks

    There are no required textbooks but we'll use lecture notes and supplementary research papers and manuscripts. See our course reading list.

    Computers

    Programming assignments will be done using the Linux PCs in the Zoo. If you plan to take the course for credit, you should have an account on these machines.

    Grading

    Your grade will be calculated as follows: These weights are subject to minor variation.

    Attendance

    Class attendance is recommended strongly.

    Keeping In Touch

    The best way to contact the instructor and the TAs is by electronic mail. To get help quickly, your best bet is to send email to cs428ta at cs.yale.edu or cs428 at cs.yale.edu (where your message will also be forwarded to everyone in the class).

    All the course-related information will be kept at the following site: 

              http://flint.cs.yale.edu/cs428

    Copyright (c) 2009, Zhong Shao, Dept. of Computer Science, Yale University.