15-316: Software Foundations of Security & Privacy
(Spring 2023)
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 |
| Sundays and Tuesdays |
11:30 to 12:45 |
1199 |
Assignments
Homeworks
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.
In order to submit on Gradescope, your homework will need to be in PDF format.
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.
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
(15% midterm, 15% final) |
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.
|
| Participation (10%) |
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.
Academic Integrity
You are expected to comply with the
university policy on academic integrity (see also
The Word and
Understanding Academic Integrity).
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.
Take Care of Yourself
Do your best to maintain a healthy lifestyle this semester by eating
well, exercising, getting enough sleep and taking some time to relax.
This will help you achieve your goals and cope with stress.
All of us benefit from support during times of struggle. 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 is often helpful.
If you or anyone you know experiences any academic stress, difficult
life events, or feelings like anxiety or depression, we strongly
encourage you to seek support. Counseling and Psychological Services
(CaPS-Q) is here to help: call 4454 8525 or make an appointment to see
the counselor by emailing
student-counselling@qatar.cmu.edu.
Consider reaching out to a friend, faculty or family member you trust
for help.
If you or someone you know is feeling suicidal or in danger of
self-harm, call someone immediately, day or night at 5554 7913. 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.