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 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; CS1520 is particularly useful, as many of the formalisms we use are introduced in that class).

Self Assessment: You can try this CS2540 Self Assessment to gain insight into whether you have appropriate preparation in formal reasoning and proof to take the course. Feel free to reach out to Prof Chong with questions.

Time and Place

Tuesdays, Thursdays, 12:45pm to 2pm.

Location: SEC 1.402

Course Staff

• Instructor:  Stephen Chong
• Teaching Fellows: Anastasiya Kravchuk-Kirilyu, Kevin Zhang 

When is the course typically offered?

This course will typically be offered every year in the Spring term; although there is currently a possibility that it will not be offered in Spring 2027.

Assessment

The course will have 3 homeworks during the semester, several paper discussions, 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, submission of questions/reflections for paper readings, the project, and class participation. The percentage breakdown (roughly and subject to change) is 30% homeworks, 10% reading questions/reflections, 50% final project, and 10% participation (which includes attendance and participation in class and office hours, and contributing to online discussion).

Descriptions of Harvard College's grades can be found in the Student Handbook. Here I describe what grades mean in this course.

• An A is earned by work of “extraordinary distinction", whose "excellent quality" indicates "a full mastery of the subject". In CS2540, this means:
  • Full participation in all aspects of the course (lectures, office hours, paper discussions, project groups, online forums, etc.)
  • Active engagement beyond requirements, as evidenced by, for example, asking insightful questions, contributing answers, and exploring optional/extra-credit challenges.
  • Deep understanding of the course material, including :
    • Demonstration of precise and disciplined reasoning, and appropriate use of definitions, assumptions and proof techniques.
    • Ability to clearly explain why a technique works, not just how to apply it, and to articulate trade-offs among alternative formalisms and approaches.
    • Identification and discussion of subtle assumptions, limitations, or edge cases in formal models or security arguments.
  • An extraordinary project, including:
    • A clear, well-defined, and well-motivated problem.
    • A thorough search of related literature and a meaningful comparison of that related work to the student's project.
    • Appropriate application of the course's concepts and techniques.
    • Presentation and writing quality at the level of a strong workshop or conference submission.

• An A– is earned by work whose "excellent quality" indicates a “full mastery of the subject.” In CS2540, this means:
  • Consistent participation in the course (lectures, office hours, paper discussions, project groups, online forums, etc.)
  • Active engagement beyond requirements, as evidenced by, for example, asking insightful questions, contributing answers, and exploring optional/extra-credit challenges.
  • Strong understanding of the course material, including:
    • Largely correct and well-reasoned homework solutions, with only minor gaps or imprecision.
    • Ability to correctly apply course concepts and techniques, and to explain their use, though with less depth, generality, or independence than required for an A.
  • A strong project, including:
    • A clear, well-defined, and well-motivated problem.
    • Engagement with relevant related work, with appropriate (though possibly limited) comparison.
    • Correct application of course concepts and techniques.
    • Clear presentation and writing, though not necessarily at the level of a polished research submission.

• A B+, B, or B– is earned by work that indicates a “good comprehension of the course material, a good command of the skills needed to work with the course material, and the student’s full engagement with the course requirements and activities." In CS2540, this means:
  • Regular attendance and timely completion of all homeworks.
  • Homework solutions that are generally correct but may contain errors, gaps in reasoning, or imprecise use of formal definitions.
  • Ability to apply course techniques to standard problems, with limited ability to extend, generalize, or critique those techniques.
  • A completed project that:
    • Addresses a reasonable problem or topic.
    • Makes use of relevant course concepts.
    • Demonstrates effort and understanding, but lacks the depth, rigor, or originality expected for an A-range grade.
      

• A C+, C, or C– is earned by work that indicates an “adequate and satisfactory comprehension of the course material and the skills needed to work with the course material." In CS2540, this means:
  • Inconsistent participation or limited engagement with course activities; completion of nearly all homeworks. 
  • Homework solutions that demonstrate familiarity with the material but include significant errors, omissions, or misunderstandings.
  • Difficulty applying formal methods or security concepts without substantial guidance.
  • A minimally acceptable project that:
    • Is incomplete, poorly scoped, or weakly motivated, or
    • Demonstrates limited understanding of the relevant course concepts and techniques.

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 and attendance will be taken.. 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 discuss more at the beginning of the course.

Simultaneous Enrollment

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

Homeworks

Projects are done individually. See below for the collaboration policy. All students should respect the Harvard academic integrity policy and the course collaboration policy.

Project

Please see the Project Guide page for more information about projects.

Late minutes, Penalties, and Extensions

Each student will have 7,200 “late minutes” (which is the number of minutes in 5 days) which can be applied to any of the homeworks. 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 homework. (This allows us to grade your homeworks and return them to you within a reasonable period.)

Late minutes can not be used for final project deadlines or for paper reflections.

Late minutes are intended to help you manage your time effectively. They are not meant to be a substitute for starting homeworks 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.

Calendar

This calendar shows the lectures and office hours in this course. We will try to keep this calendar up to date, but please also pay attention to announcements on Ed in case someone needs to cancel their OH. See also the Schedule, which includes lecture topics and key course deadlines.

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.

Inclusive Learning and Accessibility

Your success in this class is important to me. If there are aspects of this course that prevent you from learning or exclude you, please let me know as soon as possible.

I encourage you to visit the Disability Access Office to determine how you could improve your learning; if you need official accommodations, you have a right to have these met.

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.

There are also a range of resources on campus. The Academic Resource Center provides many resources, including academic counseling and peer tutors. 

Mental Health

If you experience significant stress or worry, changes in mood, or problems eating or sleeping this semester, whether because of CS2540 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 nor accept them from another student. For programming problems, 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.