15-316: Software Foundations of Security & Privacy (Spring 2024)
Overview
Security and privacy issues in computer systems continue to be a
pervasive issue in technology and society. Understanding the security
and privacy needs of software, and being able to rigorously demonstrate
that those needs are met, is key to eliminating vulnerabilities that
cause these issues. Students who take this course will learn the
principles needed to make these assurances about software, and some of
the key strategies used to make sure that they are correctly implemented
in practice. Topics include: policy models and mechanisms for
confidentiality, integrity, and availability, language-based techniques
for detecting and preventing security threats, mechanisms for enforcing
privacy guarantees, and the interaction between software and underlying
systems that can give rise to practical security threats. Students will
also gain experience applying many of these techniques to write code
that is secure by construction.
Learning goals
The philosophy underpinning this course seeks 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.
Pre-requisites
15-213 (Introduction to Computer Systems) with a C or better.
Credits
This is a 9 unit elective course.
Place and time
Day
Time
Location
Mondays and Wednesdays
11:30 to 12:45
CMB 1199
Schedule
Note: to compile lecture notes, you will need to download the
latex packages and place
the .sty files in the same directory as the lecture source.
Thursdays, 9:00am - 1:00pm by appointment.
(The appointment is mostly so that I know you are coming and don't book something else into the slot.)
Open Door Policy: If my office door is open (or partially open
with a door stop), feel free to knock and come in. If it is
fully closed, then I am not available for office hours, even
if I am in the office.
By custom appointment. (Feel free to email me to setup a time to meet if neither of the above work.)
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.
Unless otherwise stated, all homeworks are due at 8:00pm on the date
marked on the handout. Written 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.
Homework submissions will be on Gradescope, and your submission must be
a professional looking PDF file. The quality should be something that
you would be proud to show to others in a workplace or academic setting.
Submissions that are not sufficiently professional in appearance will
not be graded.
You are strongly encouraged to typeset your homework using
LaTeX. Typically you will edit a .tex file
which
is compiled
into a pdf. This file uses specific tags and commands for typesetting.
If you only know Word (or similar) for creating documents, LaTeX takes a
little getting used to, but it is worth it. After you become familiar
with the syntax, some advantages are:
Typing math is much (much, much) faster
You do not have to worry about margins or consistent style of headers
or alignment
Changing the order of sections involves no renumbering on your part
References are formatted and numbered for you (APA? What is that?)
There are various tools for editing and compiling LaTeX. If you do not
want to install anything locally, you can use one of the web-based ones,
such as Overleaf. If you use Overleaf, upload all files in the
latex
directory of the handout. 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.
As with homeworks, all labs are due at 8:00pm on the date marked on the
handout. Labs should also be submitted on Gradescope.
Discord
We will be using Discord this semester as the course discussion board
and question and answer forum. You should have received an invite to the
course Discord server during the first week of classes.
If you have never used Discord before, consider the following tips:
If you are creating a Discord account, it is probably a good idea
not to use your real name as your username or overall display
name.
Once you join the class Discord server, there are rules that you will
need to agree to. You will also need to change your
Server Nickname to be your real name. (Don't worry, this server
nickname is only for this class. Your username
and display name on other parts of Discord are unaffected.)
You should download and install the Discord app on your computer (or
phone or tablet). This will ensure you get notifications whenever
there are announcements and notifications about the course.
If you have used Discord before, feel free to use your existing account.
However, please note that your Discord username will be visible with
your profile, even after you change your server nickname. (So if having
other people see your Discord username would be embarrassing, then keep
that in mind...)
Policies
Grading
Your final grade will be calculated using the following weightings:
Component
Description
Labs (30%)
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.
Homework (30%)
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.
Exams (35%)
We will have two exams. The content of these exams will more
closely resemble the written homework than the labs, but some
questions may rely on, or make reference to, key parts of the
labs. The midterm will take place during the normal class
meeting time, in the same room used for lectures. Both exams are
"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 (by you) notes. Typed or photocopied notes
will not be allowed.
Your highest scoring exam will be weighted at 20%, and your
lowest scoring exam weighted at 15%.
Participation (5%)
Active class participation counts for a small percentage of your
grade, and in borderline letter-grade cases, could be decisive of
what ultimately appears on your transcript. This is a relatively
small course, so we expect to become familiar with each of you
through your lecture attendance. Some factors that we will use to
decide the participation component are attendance, interaction
through good questions and answers during class discussions.
Although you are not required to make use of Piazza, we appreciate
students who are willing to help others by answering questions and
providing helpful advice, and doing so will factor into your
participation grade.
Regrades
We occasionally make mistakes while grading (we're only human!). If you
find a mistake which you would like us to correct, then submit a regrade
request using the Gradescope regrade request feature. Regrades must be
requested within two weeks of the time when the contested grade was
released. The two week limit may be shortened at the end of the semester
in order to meet grade submission deadlines.
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.
And remember not to ignore your inner voice when it says "That's
probably not the best decision...".
An Invitation to Students with Learning Disabilities
Carnegie Mellon University is committed to providing reasonable
accommodations for all persons with disabilities. To access
accommodation services you are expected to initiate the request and
submit a Voluntary Disclosure of Disability Form to the office of Health
& Wellness or CaPS-Q. In order to receive services/accommodations,
verification of a disability is required as recommended in writing by a
doctor, licensed psychologist or psycho-educational specialist. The
office of Health & Wellness, CaPS-Q and Office of Disability
Resources in Pittsburgh will review the information you provide. All
information will be considered confidential and only released to
appropriate persons on a need to know basis.
Once the accommodations have been approved, you will be issued a Summary
of Accommodations Memorandum documenting the disability and describing
the accommodation. You are responsible for providing the Memorandum to
your professors at the beginning of each semester.
We all feel stress at different times and for different reasons, and when we do, it is good to reach out for
support. Do your best to maintain a healthy lifestyle by eating well, exercising, getting enough sleep and
taking some time to relax. Please know that 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. Asking for support
sooner, rather than later, can often help your situation from getting more complicated. If you or any of your
CMUQ peers are experiencing academic stress, difficult life events, or feelings like anxiety or depression, we
strongly encourage you to seek support.
Our Student Affairs staff are here to help:
Dr. Dalia Rehal, Associate Dean for Student Affairs (CMB 1094), drehal@qatar.cmu.edu, 4454-8545
Amie Rollins, Office of Health and Wellness (CMB 1103), amier@andrew.cmu.edu, 4454-8680
Dr. Atorina Benjamin, Counseling and Psychological Services (CMB 1104), atorinab@qatar.cmu.edu, 4454-8525
You can also visit the Ilona Wyers Student Lounge and connect with anyone on the Student Affairs Team. Consider
also reaching out to a friend, faculty, staff, or family member you trust for help.
If you would like to speak to a trained professional for mental health support, day or night, call our ProtoCall
hotline at 5554 7913, which is staffed by trained mental health care providers.
If the situation is life threatening, call 999.
Diversity Statement
It is my hope that students from a diversity of backgrounds and
perspectives be well served by this course, that students' learning
needs be addressed both in and out of class, and that the diversity
students bring to this class be viewed as a resource, strength and
benefit. It is my intent to present materials and activities that are
respectful of diversity: gender, sexuality, disability, age,
socioeconomic status, ethnicity, race, nationality, religion, and
culture. Your suggestions are encouraged and appreciated. Please let me
know ways to improve the effectiveness of the course for you personally
or for other students or student groups.
This statement is adapted from The
University of Iowa Department of
Education.