COMPSCI 254: Formal Methods for Computer Security
This course explores formal methods for computer security, including formal security models, relationships between security properties/policies and enforcement mechanisms, principled techniques and tool to specify, analyze, and construct secure computer systems. Specific topics include properties, hyperproperties, side channels, reasoning about cryptographic protocols, information flow, authorization logics, and verification techniques. Assessment will include homeworks and/or small projects during the semester as well as a final, larger project that is open-ended and driven by student interests.
- Understand fundamental concepts and principles of formal methods in computer security, including specification of models for computational systems, attacker ability, desirable security properties of the system, and proof that a given mechanism enforces the desired security property.
- Gain knowledge of different formalisms used in computer security, such as mathematical logic, authorization logics, trace-based specifications, and program correctness triples.
- Acquire proficiency in applying formal methods and tools to analyze and reason about the security properties of software systems, such as cryptographic protocol analyzers, security type systems, theorem provers, model checkers, and symbolic executors.
- Understand some of the limitations and challenges of applying formal methods in computer security and the trade-offs between formal verification and other security assurance techniques.
This course is suitable for graduate students and advanced Computer Science undergraduates. Undergraduates should be comfortable with programming (e.g., CS51 or more advanced), systems (e.g., CS61 or more advanced), and formal reasoning and proofs (at least two #formalreasoning courses).
When is the course typically offered?
This course will typically be offered every year in the Spring term.
The course will have 3-5 homeworks/projects during the semester, and a final, larger project that is open-ended and driven by student interests.
Your grade will be determined by a weighted average of your scores on homeworks/projects, the final exam, and class participation. The percentage breakdown (roughly and subject to change) is 50% homeworks/projects, 40% final project, 10% participation (which includes attendance and participation in class and office hours, and contributing to online discussion).
Expectations and Policies
The following sections describe expectations and policies for students in this course, as well as what you can expect from the course staff. Please get in touch if anything isn't clear.
Attendance at lecture is expected. We may record lectures, and if so, students can watch lecture videos on demand, which are typically available within 24 hours of the lecture. However, the lecture videos complement but do not substitute for attending class in person.
All students are expected to stay up to date on the course material, either by reading the lecture notes, by watching the lecture video, and/or talking with classmates, as the projects are based on material covered in lectures.
Devices in class: I appreciate that different people learn differently. For some students, using a device in class can be an effective learning aid (for example, to take notes). However, for many students, laptops and smart phones are a distraction. I encourage you to bring or use electronic devices with you to class only if you think it will improve your learning. We will have part of the room reserved to be device free.
Simultaneous enrollment in this course will not be possible, sorry.
Projects are done individually: you must write all your own code. Do not share code with others (including letting others look at your code), do not accept code from others, and do not look for code online. However, you are encouraged to talk about the project with others, to share ideas and thoughts. All students should respect the Harvard academic integrity policy and the course collaboration policy below.
Late minutes, Penalties, and Extensions
Each student has 14,400 “late minutes” (which is the number of minutes in 10 days) which can be applied to any of the homeworks/projects, except for the final project. A late minute extends the due date/time by 1 minute. At most 4,320 late minutes (= 3 days) can be used on any single project. (This allows us to grade your projects and return them to you within a reasonable period.)
Late minutes are intended to help you manage your time effectively. They are not meant to be a substitute for starting homeworks and projects early.
Late minutes are not meant to be used for health issues (including mental health issues), family emergencies or other extenuating circumstances. In those situations, please contact the instructor.
You should come to office hours! Office hours are a great opportunity to participate in the course and get to know course staff and other students!
You don't need to do much or any preparation to attend office hours. You are welcome to ask any kind of question: about understanding the material covered in lecture or in projects, about extensions to the ideas presented in the course, about how the material applies beyond the course, etc. You are welcome to work on your project during office hours but note that course staff may need to attend to other students during the office hours and may not be able to help you debug your code.
Office hours in this course are drop-in: you do not need to make an appointment; it is fine to just show up.
If you would like to attend office hours but can’t, please let us know! We can attempt to adjust our office hours, or to arrange a separate time to meet.
If you find that you are struggling with understanding the material, or do not have enough time to spend on this course, or if there is anything going on in your life that is affecting your engagement with the course, please get in touch. We would rather hear from you early and often than only hear from you when you are in crisis.
Diversity and Inclusion
Some text for this course's policies is based on material by Monica Linden, Neuroscience, Brown University and David Malan, Computer Science, Harvard University.
I would like to create a learning environment that supports a diversity of thoughts, perspectives and experiences, and honors your identities (including race, gender, class, sexuality, religion, ability, etc.) To help accomplish this:
- If you have a name and/or set of pronouns that differ from those that appear in your official Harvard records, please let me know!
- If you feel like your performance in the class is being impacted by your experiences outside of class, please don't hesitate to come and talk with me. I want to be a resource for you. If you prefer to speak with someone outside of the course, the SEAS Office of Diversity, Inclusion, and Belongingmay be a useful starting point.
- I (like many people) am still in the process of learning about diverse perspectives and identities. If something was said (by anyone) in class, office hours, online discussion, or project group work that made you feel uncomfortable, please talk to me about it.
- As a participant in course discussions, office hours, and group projects, you should also strive to honor the diversity of your classmates.
If you ever are struggling and just need someone to talk to, feel free to stop by office hours, or to reach out to me and we can arrange a private meeting.
Inclusive Learning and Accessibility
Your success in this class is important to me. We will all need accommodations because we all learn differently. If there are aspects of this course that prevent you from learning or exclude you, please let me know as soon as possible. Together we'll develop strategies to meet both your needs and the requirements of the course.
I encourage you to visit the Disability Access Office to determine how you could improve your learning as well. If you need official accommodations, you have a right to have these met. There are also a range of resources on campus. The Academic Resource Center provides many resources, including academic counseling and peer tutors.
If you have a letter from the Disability Access Office, please try to get that to me earlier rather than later. Concretely, please try to give it to me by the end of the second week of classes.
If you experience significant stress or worry, changes in mood, or problems eating or sleeping this semester, whether because of CS153 or other courses or factors, please do not hesitate to reach out immediately, at any hour, to any of the course staff to discuss. Everyone can benefit from support during challenging times. Not only are we happy to listen and make accommodations with deadlines as needed, we can also refer you to additional support structures on campus, including, but not limited to:
- CAMHS Cares 24/7 Mental Health Support Line for Students, 617-495-2042
- Room 13, 617-495-4969
We do not require that students purchase any books, hardware, or software. While not required, having one's own laptop is helpful. Students without their own laptops are encouraged to reach out at the start of the course to discuss possibilities.
Discussion and the exchange of ideas are essential to doing academic work. In this course, you are encouraged to consult with your classmates as you work on homeworks and projects. However, after discussions with peers, make sure that you can work through the problem yourself and ensure that any answers you submit for evaluation are the result only of your efforts. In addition, you must cite any books, articles, websites, lectures, etc. that have helped you with your work using appropriate citation practices. Similarly, you must list the names of students with whom you have collaborated on problems.
Do not pass solutions to homeworks or projects nor accept them from another student. For programming projects, this means do not share code. Do not post course materials (including problem sets, solutions, exams, etc.) to websites (including public GitHub repositories, and similar) or course-content archives. Also, it is never okay to look up solutions to homework problems in this class, i.e., don't look on the web for solutions.
You can definitely engage in "high level" discussions with your peers, for example, about the problem statement. You can definitely engage in "low level" discussions with your peers, for example, about syntax and libraries, compiler error messages, etc. "Mid level" discussions require discretion and should be limited in this course.
If you are ever in doubt, ask the course staff to clarify what is and isn't appropriate.
The syllabus page shows a table-oriented view of the course schedule, and the basics of course grading. You can add any other comments, notes, or thoughts you have about the course structure, course policies or anything else.
To add some comments, click the "Edit" link at the top.