Software Foundations of Security & Privacy
Contact the course staff: firstname.lastname@example.org
TAs: Jiaqi Liu, Victor Song
- Time slots TBD
- Tuesday/Thursday 8:35-9:55
- Margaret Morrison A14
There is no textbook for this class. Lecture notes will be posted to the course website, but be aware that they may not contain everything covered in class. Comments and corrections are welcome, please give them to the course staff on Piazza.
Consult the online schedule for up-to-date information.
This course aims to bridge formal principles with their practical application to enhancing security and privacy in software implementations. On the “principles” side, there are several key learning objectives.
Identify and formalize security and privacy policies. In order to reason about vulnerabilities in software, and ultimately demonstrate their absence, we need to agree on what it means for the code to satisfy security and privacy requirements. Students will learn how to formalize these policies using logical specifications, types, and mathematical definitions that give precise meaning to policies.
Understand formal proof and deductive systems. One of the key benefits of formalizing policies is that it becomes possible to conduct formal proof of a program's adherence to policy. Formal proofs can be checked by automated procedures, and in many cases can be derived automatically or with substantial assistance from automated tools. Students will understand the properties of deductive systems that lead to their useful application in software security, be able to establish these properties for novel deductive systems, and be able to conduct a formal proof that a piece of software adheres to a security policy.
Understand how automated software security tools work. Most of the tools and techniques that are discussed in this class are not perfect, and will never be able to meet all security needs in all settings. Understanding the principles and techniques that these tools use is necessary for evaluating when it is appropriate to use then, and for addressing their limitations in practice.
However, this is not a "pure" theory course, and much of the intended focus is on applying the above principles to real, practical problems that arise in software security and privacy.
Apply rigorous techniques to achieve security and privacy. The course will cover numerous techniques for translating the objectives of formal policies into practical implementations that meet these objectives. Students will learn how to use reference monitors, type systems, authorization logic, and state space exploration to ensure that implemented code satisfies a given policy.
Understand trusted computing technologies. Trusted computing and related technologies are widely used in practice, and continue to show promise in emerging "killer" applications. Students will understand how the formal principles underpinning this technology yield practical, scalable results through the use of hardware protections and software techniques that build on them.
Understand web security threats & best practices. Ensuring that web applications are robust against attack and manage users' private data correctly is a challenging problem that many developers will face at some point in their work. Many of the techniques and principles covered in this course are illustrated with practical examples from web security, and students will learn about the prevailing security models in this domain as well as several techniques for ensuing that application-specific security needs are met.
At all times, the interplay between attack and defense is central to the topics covered in this course. We will not spend much time is this course writing exploits for known vulnerabilities, but it is often the case that in order to design an appropriate defense, intimate knowledge of the attacker's design space and toolbox is necessary. Conversely, students will learn that once one has formalized a security policy and semantics for the system, it becomes easy to identify potential vulnerabilities, or to rule out entire classes of potential vulnerability. In short, students will not learn specific hacking techniques in this course, but will understand how to identify and analyze software vulnerabilities for the purpose of designing mitigations.
We enjoy seeing you in class, so please come to the lectures unless you have an unavoidable conflict, in which case you are expected to follow up with what you have missed in class on your own. Although class participation only counts for a small portion of your grade, it can be enough to sway a final letter grade in certain circumstances. Please sit near the front, interact, and ask questions. This is the best way to learn!
As research on learning shows, unexpected noises and movement automatically divert and capture people’s attention, which means you are affecting everyone’s learning experience if your phone, laptop, etc. makes noise or is visually distracting during class. You may use laptops for taking notes, but if the course staff notices other content on your screen that may be distracting for you or others—news, videos, games, or even other homework—we will ask you to put the device away for the rest of the lecture.
Assignments, exams, and grading
Grading will be based on labs, written homework, midterm and final exams, and class participation. Barring exceptional circumstances, letter-grade thresholds are: 90% (A), 80% (B), 70% (C), 60% (D).
The lab assignments are designed to give you hands-on experience writing secure software that serves a practical purpose. In general, the lab assignments will ask you to implement some functionality (generally in C) related to a network server that receives HTTP requests, while ensuring that it is not vulnerable to a particular class of security threats. Some of the labs will give you hands-on experience using tools to help achieve this goal, whereas others will have you implementing a technique discussed in lecture.
The most important criterion with respect to grading the labs is correctness, and your justification for believing that your solution is correct. An ideal lab attempt contains a concise, correct security policy, and a correct implementation of an apparatus that enforces that policy or sufficient documentation of the steps you took to ensure compliance. However, it may be the case that your policy is incorrect, or too complicated for the grader to fully understand. Verification of policy to code cannot be fully automated, so it is possible that the grader is not able to certify that your solution is guaranteed to be correct. In these cases, you will receive partial credit, so it is also important that the code you hand in be clean and well-commented, as course staff cannot assign points to solutions that they do not understand.
Labs will be handed in on Gradescope.
Written homework will be assigned more frequently, and should not require as much time to complete as the labs. The goal of the written homework is to help you refine the fundamental skills, and better understand the theoretical underpinnings, that you will need in order to do well on the labs and exams. Grading for these assignments is based on the correctness of your answer, and the presentation of your reasoning. You should strive for clarity and conciseness, while making sure to show each step of your reasoning. Categorical answers with no explanation will not even receive partial credit, but lucid explanations of your attempt to find the answer will.
Written homework will be handed in via Gradescope, and should preferably be typeset in LaTeX. Alternatively, you can (neatly) write your solutions on paper, and photograph or scan them. Homework that the course staff cannot read will not receive any points.
Final Exam (20%)
We will have an in-person final exam, with questions that resemble the written homework and in-class quizzes. The final is "closed book" (i.e., you may not reference our lecture notes), but you are allowed to bring a single double-sided sheet of hand-written notes.
During regular class meeting times, we will hand out a brief quiz covering topics from recent lectures. Quizzes will be given most weeks of the semester, with up to one quiz per week. Students are expected to complete quizzes without consulting notes, and any formulas, definitions, or proof rules needed to complete them will be handed out along with the quiz.
For special accommodations on exams, students should submit an accommodations letter to the course staff at least one week before. For extra time on exams we then ask that you arrange it to be proctored through the disability services office (assuming you have given us the form) for each exam separately. We will work with them to get them a copy of the exam. For other issues please contact the instructor. No make up exams are given, except for medical reasons. To schedule a make-up exam, ask your academic advisor to contact the instructors. Please do not email the course staff personally. You will need to provide medical documentation that shows that you cannot take the exam.
Homework and lab assignments should be submitted by the date marked on the course website. For assignments handed in past that date, 10% of the total possible points will be deducted for each late day, up to three total late days.
When you need help from the course staff, please use Piazza first. If you feel that Piazza is not appropriate, then you can email the instructor. Of course you are always welcome to office hours, or to ask the TAs or instructor questions after class, time permitting.
How to use Piazza: We will post announcements, clarifications, corrections, and hints on Piazza, and in certain cases to the course webpage. When using Piazza for discussion of labs and homework, please resist the temptation to ask every question that you might have. Even with a moderately-sized course like this one, the volume of traffic can get out of hand, making it difficult for course staff and other students to keep up. Most importantly, the best way to learn this material is to spend time thinking through the details yourself, and exploring various alternative solutions. Asking others for too many hints contradicts that process, and will leave you less well-prepared for exams and future labs.
Please make your Piazza questions public. Chances are that other students have similar questions to the one you're asking, and marking it private will likely require the course staff to spend unnecessary time posting responses to several minor variations of the same question. A good heuristic to use is that if you don't feel comfortable making your question public, then Piazza might not be the right place to ask it. In these cases, emailing the course staff, or coming to office hours, may be the right thing to do.
Students are expected to complete each assignment on their own, and should be able to explain all of the work that they hand in. Copying code or proof material from other students or online sources is not allowed. However, students are encouraged to discuss assignments with each other at a sufficiently high level to avoid the risk of duplicating implementation or proof. Examples of this would be discussing algorithms and properties referred to in the assignment, helping other students with questions about a programming language or tool required to complete the assignment, discussing a general proof technique, or referring to an online source with useful information. If you have questions about whether something might be an issue, contact the course staff before discussing further. Please refer to the Carnegie Mellon Code for information about university policies regarding academic conduct.
Carnegie Mellon University makes every effort to provide accessible facilities and programs for individuals with disabilities. If you have a disability and require accommodations, contact the Office of Disability Resources at email@example.com. Please let the instructors know early in the semester so that your needs may be appropriately met. Special accommodation for exams must be requested for each exam separately one week in advance.
Take Care of Yourself
All of us benefit from support during times of struggle, and the unusual situation that we are in this semester certainly amplifies the chance that you will find yourself in a difficult place. You are not alone. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. You should ask sooner rather than later. Should you find yourself or a friend in serious trouble, take it seriously: your classes can wait. For emergencies call UPMC’s re:solve Crisis Network at
. Counseling and Psychological Services (CaPS) is here to help: call
and visit their website at
. Also consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.