LangSec slides.
This commit is contained in:
Justin Hsu
parent
d91d8681e7
commit
f27ef83f20
|
|
@ -0,0 +1,182 @@
|
||||||
|
---
|
||||||
|
author: Topics in Security and Privacy Technologies (CS 839)
|
||||||
|
title: Language-Based Security
|
||||||
|
date: November 21, 2018
|
||||||
|
---
|
||||||
|
|
||||||
|
# LangSec: Principles
|
||||||
|
|
||||||
|
## Programs are written in programming languages
|
||||||
|
|
||||||
|
## Security holes are bugs
|
||||||
|
1. Programmer writes some code
|
||||||
|
2. Programmer makes a mistake!
|
||||||
|
- Forgot to check permissions
|
||||||
|
- Mixed private and public data
|
||||||
|
- Didn't allocate enough space
|
||||||
|
- ...
|
||||||
|
3. Attacker exploits the security flaw
|
||||||
|
|
||||||
|
## Programming languages: <br> first line of defense
|
||||||
|
- Catching errors earlier is better
|
||||||
|
- Earliest possible time: when program is written
|
||||||
|
- Easier to reject program than try to protect against it
|
||||||
|
|
||||||
|
## Design languages <br> to reduce security flaws
|
||||||
|
- Make it easier for programmer to do right thing
|
||||||
|
- Make certain kinds of bugs impossible
|
||||||
|
- Limit damage caused by any bugs
|
||||||
|
|
||||||
|
## When are errors caught?
|
||||||
|
- When the program is running
|
||||||
|
- Stop program when it does something unsafe
|
||||||
|
- "Dynamic analysis"
|
||||||
|
- When the program is compiled
|
||||||
|
- Reject bad program before it even runs
|
||||||
|
- "Static analysis"
|
||||||
|
|
||||||
|
# Overall Strategy
|
||||||
|
|
||||||
|
## 1. Pick a language
|
||||||
|
- Real languages: Java, C, ...
|
||||||
|
- Highly complex: tons of features
|
||||||
|
- Hard to modify language
|
||||||
|
- Idealized "core" languages
|
||||||
|
- Much simpler, small number of features
|
||||||
|
- Model "essence" of real languages
|
||||||
|
|
||||||
|
## 2. Formalize what programs "do"
|
||||||
|
- Usually: run it on a machine and find out!
|
||||||
|
- Not very useful for proofs...
|
||||||
|
- Formalize behavior mathematically, on paper
|
||||||
|
- Discard "unimportant" details
|
||||||
|
- Describe how program "steps"
|
||||||
|
|
||||||
|
## 3. Describe how to check <br> a given program
|
||||||
|
- Must work *without* running the program
|
||||||
|
- Other desirable features:
|
||||||
|
- Scales up to large programs
|
||||||
|
- Runs in a reasonable amount of time
|
||||||
|
- Doesn't reject too many correct programs
|
||||||
|
|
||||||
|
## 4. Prove correctness
|
||||||
|
- We want to prove two things:
|
||||||
|
- Soundness: catch all buggy programs
|
||||||
|
- Completeness: accept all correct programs
|
||||||
|
|
||||||
|
> Almost always: can't have both!
|
||||||
|
|
||||||
|
## Usually: pick soundness
|
||||||
|
- All buggy programs are rejected
|
||||||
|
- If the check says "safe", then it is safe
|
||||||
|
- But: some safe programs might be rejected
|
||||||
|
- Hopefully, not too many
|
||||||
|
|
||||||
|
# Imperative Languages
|
||||||
|
|
||||||
|
## Most familiar
|
||||||
|
- Basis of many popular languages
|
||||||
|
- Java, C++, Python, ...
|
||||||
|
- Program executes sequence of instructions
|
||||||
|
- Can read/write to *variables*
|
||||||
|
|
||||||
|
## Keep essential features
|
||||||
|
- Assignments to variables
|
||||||
|
- Sequencing ("semicolon")
|
||||||
|
- Conditionals ("if-then-else")
|
||||||
|
- Loops
|
||||||
|
|
||||||
|
## Drop fancier features
|
||||||
|
- Memory management
|
||||||
|
- Jumps and gotos
|
||||||
|
- Function pointers
|
||||||
|
- Templates
|
||||||
|
- ...
|
||||||
|
|
||||||
|
## Example
|
||||||
|
|
||||||
|
# Functional Languages
|
||||||
|
|
||||||
|
## Maybe a bit less familiar
|
||||||
|
- No imperative features
|
||||||
|
- Can't modify variables
|
||||||
|
- Usually no looping command (instead: recursion)
|
||||||
|
- Instead: functions
|
||||||
|
- Define functions
|
||||||
|
- Call ("apply") functions on arguments
|
||||||
|
|
||||||
|
## Simpler to formalize
|
||||||
|
- Program includes "all the information"
|
||||||
|
- Behavior doesn't depend on state of variables
|
||||||
|
- Program "runs" by changing the code itself
|
||||||
|
- Simplifies all the way down to final answer
|
||||||
|
|
||||||
|
## Example
|
||||||
|
|
||||||
|
# Operational Semantics
|
||||||
|
|
||||||
|
## Programs execute by "stepping"
|
||||||
|
- Start with program
|
||||||
|
- Imperative: plus variable setting
|
||||||
|
- In each step, perform update:
|
||||||
|
- Functional: modify the program
|
||||||
|
- Imperative: update variables
|
||||||
|
- Terminates when it stops stepping (is a "value")
|
||||||
|
|
||||||
|
## Example
|
||||||
|
|
||||||
|
## Different styles
|
||||||
|
- Big-step
|
||||||
|
- Describe value a program eventually steps to
|
||||||
|
- Small-step
|
||||||
|
- Describe one step of a program
|
||||||
|
|
||||||
|
# Type Systems
|
||||||
|
|
||||||
|
## Assign "types" to programs
|
||||||
|
- A type $\tau$ describes a class of programs
|
||||||
|
- Usually: well-behaved in some way
|
||||||
|
- Can automatically check if program has type $\tau$
|
||||||
|
- Type of program depends on types of its pieces
|
||||||
|
- Scales to large programs
|
||||||
|
|
||||||
|
## Example
|
||||||
|
|
||||||
|
## Strengths
|
||||||
|
- Lightweight
|
||||||
|
- Checking types is simple, automatic
|
||||||
|
- Don't need to run program
|
||||||
|
- Intuitive meaning
|
||||||
|
- Can't add a String to a Boolean
|
||||||
|
- Programmers often think in terms of types
|
||||||
|
- Identify correct programs
|
||||||
|
|
||||||
|
## Weaknesses
|
||||||
|
- Programmer may need to add some type hints
|
||||||
|
- Extra annotations in program
|
||||||
|
- Common for more complex types
|
||||||
|
- Compiler sometimes rejects correct programs
|
||||||
|
- Figuring out why can be very frustrating
|
||||||
|
- May need to write program in more awkward form
|
||||||
|
|
||||||
|
## Types can be complex
|
||||||
|
- Simpler types
|
||||||
|
- String, Char, Bool, Int, function types, ...
|
||||||
|
- More complex types
|
||||||
|
- Secret values/public values
|
||||||
|
- Trusted values/untrusted values
|
||||||
|
- Local data/remote data
|
||||||
|
- Random values
|
||||||
|
- ...
|
||||||
|
|
||||||
|
## Prove: soundness
|
||||||
|
- "Soundness theorem"
|
||||||
|
- Relate type system to operational behavior
|
||||||
|
- If program has a type, it should be well-behaved
|
||||||
|
- Many possible notions of "well-behaved"
|
||||||
|
- Don't add Strings to Bools
|
||||||
|
- Don't mix public and private data
|
||||||
|
- Don't write past end of buffer
|
||||||
|
- ...
|
||||||
|
|
||||||
|
> "Well-typed programs can't go wrong"
|
||||||
|
|
@ -33,7 +33,7 @@ Data Privacy* (AFDP) by Cynthia Dwork and Aaron Roth, available
|
||||||
11/14 | Verifiable differential privacy <br> **Paper:** Narayan, Feldman, Papadimitriou, and Haeberlen. [*Verifiable Differential Privacy*](https://www.cis.upenn.edu/~ahae/papers/verdp-eurosys2015.pdf). <br> <center> <h5> **Due: Milestone 2** </h5> </center> | Fayi
|
11/14 | Verifiable differential privacy <br> **Paper:** Narayan, Feldman, Papadimitriou, and Haeberlen. [*Verifiable Differential Privacy*](https://www.cis.upenn.edu/~ahae/papers/verdp-eurosys2015.pdf). <br> <center> <h5> **Due: Milestone 2** </h5> </center> | Fayi
|
||||||
11/19 | Homomorphic encryption <br> **Paper:** Halevi and Shoup. [*Algorithms in HElib*](https://www.shoup.net/papers/helib.pdf). | Yue
|
11/19 | Homomorphic encryption <br> **Paper:** Halevi and Shoup. [*Algorithms in HElib*](https://www.shoup.net/papers/helib.pdf). | Yue
|
||||||
| <center> <h4> **Language-Based Security** </h4> </center> |
|
| <center> <h4> **Language-Based Security** </h4> </center> |
|
||||||
11/21 | Language-based security: overview and basics | Justin
|
11/21 | [Language-based security: overview and basics](../resources/slides/lecture-langsec.html) | Justin
|
||||||
11/26 | Languages for privacy <br> **Paper:** Reed and Pierce. [*Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy*](https://www.cis.upenn.edu/~bcpierce/papers/dp.pdf). | Sam
|
11/26 | Languages for privacy <br> **Paper:** Reed and Pierce. [*Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy*](https://www.cis.upenn.edu/~bcpierce/papers/dp.pdf). | Sam
|
||||||
11/28 | Bonus lecture on applied crypto <br> <center> **GUEST LECTURE** </center> | Somesh Jha
|
11/28 | Bonus lecture on applied crypto <br> <center> **GUEST LECTURE** </center> | Somesh Jha
|
||||||
12/3 | Languages for authenticated datastructures <br> **Paper:** Miller, Hicks, Katz, and Shi. [*Authenticated Data Structures, Generically*](https://www.cs.umd.edu/~mwh/papers/gpads.pdf). | Zichuan
|
12/3 | Languages for authenticated datastructures <br> **Paper:** Miller, Hicks, Katz, and Shi. [*Authenticated Data Structures, Generically*](https://www.cs.umd.edu/~mwh/papers/gpads.pdf). | Zichuan
|
||||||
|
|
|
||||||
Reference in New Issue