Preparation
Trustworthiness
-
Reflections on Trusting Trust, by Ken Thompson (3 pages)
-
Presents the perils of trusting software.
-
-
Putting Trust in Security Engineering, by Fred B. Schneider (3 pages)
-
Software should not only be secure. We should also have a reason to believe that the software is secure, before we can depend on it and use it. This piece proposes formal methods (FM) & programming language technology (PLT) as a means of establishing security & trustworthiness in software.
-
Language-Based Security (LBS)
-
A Language-Based Approach to Security, by Schneider, Morrisett, & Harper (14 pages)
-
Presents ways in which a software vendor can transfer trust in the correctness of the software they wrote, to a software consumer.
-
Information-Flow Control (IFC: enforcing app-specific security goals)
-
Language-Based Information-Flow Security, by Sabelfeld and Myers, Sections 1-2 (4 pages)
-
Introduction to Computer Security, by Matt Bishop, Chapter 15, 15.1-15.3, but skip 15.2.2.5, 15.2.4 (15 pages)
-
Programming in Paragon, by Delft, Broberg & Sands, Sections 1-4 (13 pages)
Exercise
Further Reading
-
Bases for Trust in a Supply Chain, by Fred B. Schneider, Section "Distinct Bases for Trust" (2 pages)
-
a newer writeup on Bases of Trust, with more examples
-
-
A Note on the Confinement Problem, by Butler Lampson (3 pages)
-
Typed Assembly Language, talk by Stephanie Weirich (56:51)
-
original papers on static & dynamic enforcement for IFC (from the 70s)
-
Certification of Programs for Secure Information Flow, by Denning & Denning
-
Memoryless Subsystems, by Fenton
-
-
From dynamic to static and back […], by Sabelfeld and Russo, Sections 2-5 (note!) (4 pages)
-
note: This is much neater than Matt Bishop’s chapter. However, to fully appreciate this, you need some background in PLT (Semantics, Types, etc.). You get that in ch. 1-7 in Bob Harper’s book. That’s out-of-scope of AIS, though.
-
Acknowledgment
Most of the slides on information-flow control are made by David Sands and Andrei Sabelfeld, from Marktoberdorf 2015 and 2011. Most of the slides on Paragon are by Niclas Broberg and Bart van Delft.