15-316: Software Foundations of Security & Privacy
(Spring 2020)
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
You must have completed 15-213 (Introduction to Computer Systems) to attend this course.
Credits
This is a 10 unit core course.
Place and time
| Day |
Time |
Location |
| Sundays and Tuesdays |
10:30 to 11:50 |
2052 |
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 11:59pm on the date marked on the handout. Also, follow announcements on Piazza for deadline updates, in case extensions are granted. 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.
If you choose not to typeset your solution, then you must print out the provided template, write your solution in the provided space, and scan or photograph it for handin on Gradescope. Handwritten homeworks will not be graded until they are on the template, and those that are handed in otherwise will be returned ungraded. If the course staff has trouble reading your handwriting, you will not receive points.
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 11:59pm 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 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 positively.
|
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.