CS 528, Fall 2014, Course Information

CS 528 Course Information, Fall 2014

Last modified: August 30, 2014.


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 operating system kernels, virtual machines, and programming languages. Language-based technologies, including program verification, formal methods, 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 language-based security techniques and show how to apply these techniques in building truly dependable system software.

CS528: Language-Based Security (Fall 2014)

TTh 2:30 PM-3:45 PM, in 000 AKW

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

Teaching Assistant:
Newman Wu, 311 Watson, office: 432-xxxx xiongnan dot wu at yale dot edu
Office hours: TBA or by appt.

Main Topics

  • Motivation and Overview
  • Hints on Programming Language Design
  • Hints and Principles for Computer System Design

  • Semantics of C and Assembly Lanuages
  • C Memory Models
  • Certified Compilers (CompCert)

  • Proof Assistant (Coq)
  • Functional Programming
  • Predicate Logics and Inductive Definitions
  • Formal Specification and Proof Objects

  • Program Refinement and Simulation
  • Hoare-Style Program Verification
  • Certified Abstraction Layers

  • Principles of Computer System Design
  • Certified OS Kernels (seL4 and CertiKOS)
  • Hypervisors and Virtualization
  • Capabilities and Access Controls
  • Inter-VM and Inter-Process Communication

  • Decentralized Information Flow Control
  • Security-Typed Programming Language

  • Interrupts and Device Drivers
  • Secure Embedded Software
  • Atomicity and Transactions
  • Concurrency and Distributed Systems

  • Textbooks

    There are no required textbooks but we'll use research papers and manuscripts from the following site:

    We will use the following ebook to learn to use the Coq proof assistant:


    Programming assignments and final projects can be done using any of your own computers or the Linux PCs in the Zoo.

    The machines in the Zoo are named as follows:

           aphid        bumblebee    cardinal    chameleon  cicada       
           cobra        cricket      frog        gator      giraffe
           grizzly      hippo        hornet      jaguar     ladybug      
           lion         macaw        monkey      newt       peacock     
           perch        python       rattlesnake rhino      scorpion    
           swan         termite      tick        turtle     viper      

    If you plan to take the course for credit, you should get an account on these machines as soon as possible. Please visit the following web site to create a cs428 class directory:

    NOTE: this step is required if you want to use the submit/unsubmit commands on the Zoo machines.


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

    Late-Assignments Policy

    Problem sets are due at 11:59 PM on the date specified.

    Each student is given 144 discretionary late hours for assignments, but any one assignment may only be up to 72 hours late. These are calendar hours, not business hours. As the homework assignments are submitted electronically, the "write date" on the student's homework file will be considered the completion date for late assignments.

    After you use up all of your discretionary late hours, assignments turned in late will be graded according to the following formula: S = R * (1 - t / c), where S is the grade given, R is the grade the work would have gotten if turned in on time, t is the amount of time by which the work was late, and c is equal to four days. Thus, the value of a late assignment decays daily, with a half-life of just over two days. Examples: work turned in five minutes late gets 99.9% credit, one hour late gets 99.0% credit, six hours late gets 93.8% credit, one day late gets 75.0% credit, two days late gets 50.0%, and three days late gets 25.0%. Assignments submitted more than 72 hours late will not be accepted.


    Class attendance is recommended strongly.

    How to Submit Assignments

    To submit your solutions to the programming assignments electronically, first change to the directory where your solutions are, and then use the following command.
         /c/cs428/bin/submit number files
    number is the assignment number and files is the list of files for that assignment. For example,
         /c/cs428/bin/submit 3 README Basics.v Induction.v
    submits the files README, Basics.v, and Induction.v for a fictitious assignment 3.

    The submit command copies your files to the directory /c/cs428/SUBMIT/number/login and lists all the files that you have submitted for assignment number. Here, login is your user account name.

    There is also unsubmit, which allows you to retract one or more files. For example,

         /c/cs428/bin/unsubmit 3 Basics.v
    would remove your Basics.v from the submission directory.

    You can also check what files you have submitted by using the check command. For example,

         /c/cs428/bin/check 3
    would list all the files your have submitted so far for assignment 3.

    Usually, you can omit the /c/cs428/bin/ prefix if /c/cs428/bin/ is already added to your PATH variable.

    Keeping In Touch

    We will use the piazza forum for announcements and discussions.

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


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