See below the table for information and policies regarding the written assignments and labs.
| assignment or lab | due date | handout | sample solution |
|---|---|---|---|
| Assignment 1: Propositional Sequent Calculus | Tue 09/10 | hw1-seq.zip | sample solution |
| Assignment 2: Dynamic Logic | Tue 09/17 | hw2-dl.zip | sample solution |
| Assignment 3: Proving Safety | Wed 09/25 | hw3-safety.zip | sample solution |
| Lab 1: Memory Safety (test cases due Tue 10/01) | Tue 10/08 | lab1-memsafety.zip |
OCaml starter code
Rust starter code
Python starter code
(binary reference solution at ~jlyao/bin/tiny_run
and ~jlyao/bin/tiny_vc on linux.andrew)
|
| Fall Break | |||
| Assignment 4: Information Flow | Wed 10/30 | hw4-infoflow.zip | sample solution |
| Lab 2: Information Flow | Wed 11/13 | (no new starter code) | |
| Assignment 5: Proof-Carrying Authorization | Wed 11/20 | hw5-pca.zip | sample solution |
| Lab 3: Proof-Carrying Authorization | Fri 12/06 | OCaml starter code Python starter code |
|
Late Policy
You have a total of 5 late days to use throughout the semester on the five written homeworks, where you may not use more than 2 days on any given homework
Each team has a total of 3 late days to use throughout the semester on the three labs, where you may not use more than 2 days on any given lab.
Written Homeworks
Homeworks are written assignments designed to help you master the theoretical concepts in this course. They will include things like logic proofs and describing vulnerabilities in formally described security systems.
Written homeworks must be done individually. Collaboration is regulated by the whiteboard policy: you can bounce ideas about a homework with other students, but when it comes to typing it down for submission, you are on your own. You are not allowed to use notes, files, pictures, etc., from any previous discussion nor previous versions of this course. If you use unrelated web resources, you must explicitly cite them.
Unless otherwise stated, all homeworks are due at 11:59pm on the date marked on the handout. Also check the announcements in Piazza for deadline updates, in case extensions are granted. All homework should be submitted through Gradescope, please notify the course staff if you have not already received an email to enroll in the relevant Gradescope instance.
In order to submit on Gradescope, your written homework will need to be in PDF format. You are highly encouraged to typeset your solutions in LaTeX, and you will find appropriate templates for each assignment below. Your graders strongly prefer LaTeX-typeset solutions, as your work is much more likely to be clear and legible, as well as consistent with the formatting they expect to see. We recognize that certain types of answers, such as those that involve graphical figures or structured formatting, can be difficult or tedious to typeset. In those cases, the template will sometimes give an example in the comments that you are encouraged to emulate, but it is fine to scan a handwritten solution to include in your latex code as a graphic.
Labs
Labs are programming assignments designed to give you hands on experience applying the concepts learned in this course. You will be writing and testing code and security policies. Labs may also involve a written part, to be handed in separately on Gradescope.
Labs may be done in pairs (strongly encouraged) or individually. If you choose to work with a partner, you should submit only one solution as a group on Gradescope. You should not collaborate with others outside your group---the whiteboard policy only applies to the written homework assignments. You are not allowed to use any materials from labs in previous versions of this course. If you use unrelated web resources, you must explicitly cite them.
As with homeworks, all labs are due at 11:59pm on the date marked on the handout. Labs should also be submitted on Gradescope.
Academic Integrity
You are expected to comply with the university policy on academic integrity for exams, and for written homeworks and labs as specified above (see also The Word and Understanding Academic Integrity).