This repository contains Tianyu's awesome PhD dissertation on gradual
information-flow control.
Topics:
- Overview
- Review of Static IFC
- Review of Dynamic IFC
- Review of Existing Gradual IFC Languages and Cast Calculi
- The Surface Language LambdaIFCStar
- The Cast Calculus LambdaIFCc
- Meta-theoretical Results and Mechanization
- Conclusion
Statements:
- Gradual IFC languages should not include \unk as a security label
on literals and values - Gradual IFC could be useful for the programmers
- IFC languages should satisfy noninterference
- NSU checking is a useful approach for enforcing noninterference (through the heap)
- Gradual languages should provide type-based reasoning
5.1 Gradual languages should be vigilant
5.2 Gradual IFC languages should perform type-guided classification - Gradual languages should satisfy the gradual guarantee
Statements about Connections:
- LambdaIFCStar does not include \unk as a runtime security label
- LambdaIFCStar is a gradual IFC language
- LambdaIFCStar satisfies noninterference (*)
- LambdaIFCStar uses NSU to enforce noninterference through the heap
- LambdaIFCStar is both vigilant and performs type-guided classification
- LambdaIFCStar satisfies the gradual guarantee
- LambdaIFCStar is type safe
Level of details:
Programmer visible details - intro - examples (show the gist; what problem is being solved?)
Details /
Implementation details - later chapters
design choice with respect to the security of the newly created memory location
Flanagan - current PC
/
- GSLRef - an interval
programmer chooses the label - ours
LambdaSEC LambdaIFCStar LambdaSEC (in Zdancewic)
|---------------|--------------------|
(dynamic) (gradual) (static)
Some final comments from the committee:
- use monospace fonts for func, addr, and diverge ✓
- define multi-step reduction ✓
- new row of the table about lambdasecstar ✓
- new intro paragraphs of section 2
- check citations of dyn IFC ✓
- check citations of static IFC ✓