CSE 130 Lecture Notes - Lecture 19: Domain-Specific Language, Llvm, Intermediate Representation
32 views5 pages
16 Mar 2018
School
Department
Course
Professor
FaCT - domain specific language for writing constant-time code
Difference between DSL and general-purpose language
- DSL more specific to A domain (SQL, FaCT, etc.)
FaCT Looks like C!
Export void conditional_swap( secret mut uint32x,
secret mut uint32 y,
secret bool cond )
Compiler generates:
- Header (.h) file - for notions of what our types are!
- Object (.o) file - link against to allow to call the function(s)
What’s in the .o? - ACTUAL implementation of the function
- spits out a LLVM - “front-end” ish, an intermediate language
- LLVM spits out all the binary bits n pieces
- “slightly” higher level than your typical assembly!
What do FaCT functions look like? (JUST functions, no main)
C-like
- Statements + expression (will have short-circuit ops!)
- Local variables + block scoping
- C-like types
- C-style “control flow”
With some differences
- secret/public annotations
- NO breaks
- NO I/O
- NO floating point
- NO raw pointers
- NO heap allocations
- NO implicit bit-widths (i.e. uint32)
How does FaCT help w/ CT?
- Mutability is explicit!
- by default vars are constant
- must declare var mut to mutate vars!
How does this help w/ CT?
- lets you know if your functions can “muck” with your arguments/variables or not!
- we should NOT let people write mutable code for immutable args/vars at compile-time!
More importantly: secrecy is explicit!
-EVERY value must be labeled secret/public
FaCT propagates labels
- secret_x + public_y is labeled secret
What about function declarations? If void, there is nothing TO return, therefore no need!
Export - can be called from C! Otherwise, you can’t call it!
How do labels help?
- Never allow secrets be written to public output!
What introduces timing channels?
1. Variable-time operators
- NO short-circuiting if operand is SECRET
- Or transform to bit-wise ops!
- NO % or / (or just emulate in software)
2. Control flow
- If (secret) → forces you to transform your code to CT!
- Secret-bounded loops!
- Early returns
- Function calls
3. Memory access patterns
- NO arr[secret]!
Labels:
- Used to prevent information leaks!
- At compile-time, type checking alg ensures that you CANNOT leak data labeled secret!
- e1 = e2 | labelOf(e1) = labelOf(e2) is context-insensitive!
- Needs to take into account whether it’s being used in a secret branch or not!
secret <- public
public <- secret
How else can we use labels?
- Restrict usage of variable-time operators!
- NO secret ops to %, |, ||, &&
- Restrict unsafe control flow
- NO branching on secrets
Giving up expressiveness ):
Can we do better?
- automatically transform statements that handle secrets to be CT!
- should we do this for EVERY unsafe pattern? NO
- hard to account for EVERY possible case!
No public assignments (in secret context)
If (secret)