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.

Learning Objectives

1. 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.
2. Gain knowledge of different formalisms used in computer security, such as mathematical logic, authorization logics, trace-based specifications, and program correctness triples.
3. 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.
4. 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.

Recommended Prerequisites

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).

Time and Place

Tuesdays, Thursdays, 11:15am to 12:30pm.

Location: SEC 2.118

Course Staff

• Instructor:  Stephen Chong
  • Office hours: Tuesdays, 1:30pm-2:30pm in SEC 4.414
    • No OH on 3/12 or 3/19. See https://people.seas.harvard.edu/~chong/schedule.html . 
• Teaching Fellows: Anastasiya Kravchuk-Kirilyuk 
  • Office hours: Wednesdays, 2pm-3pm virtually (Zoom link) and Thursdays, 3:30pm-4:30pm in-person (study area outside SEC 4.421). 

See below for office hours.

When is the course typically offered?

This course will typically be offered every year in the Spring term.

Assessment

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

Attendance in class is expected. Classes will not be recorded. Please let the instructor know if you will be missing a class.

All students are expected to stay up to date on the course material, by keeping up to date on assigned reading, reading the lecture notes, and/or talking with classmates, as the homeworks and project 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

Simultaneous enrollment in this course will not be possible, sorry.

Homeworks/Projects

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.

Office Hours

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.

Seeking Help

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.

Mental Health

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

Financial Aid

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.

Collaboration Policy

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.