Computer Science and Engineering
Secure Programming via Libraries
News
Course Information
Lectures
Exercises
Exam
Overview of the Lectures
Below you can find the material for every lecture. You can also download in a single file
print-friendly version of the slides (6 slides per page)
print-friendly version of the slides (6 slides per page) as well as the recommended papers for each day
Day 1
Introduction to the course, Haskell, and Information-flow security
Slides
Code:
Haskell overview
Code:
Examples of monad IO
Sec: a security monad for pure computations
Slides
Code:
Examples of pure computations to secure
Code:
Securing computations using monad Sec
Code:
Breaking the assumptions under which Sec can provide security
Day 2
SecIO: a security monad for side-effectful computations
Slides
Code:
Module SideEffectsSecT
Code:
Module SideEffectsSecU
Code:
Module CopyT
Code:
Module CopyU
A motivating example: a password administrator
Code:
Unsecure version
Code:
Secure version (using SecLib)
Day 3
Quick Introduction to Python
Slides
Code:
Everything is an object
Code:
Variables and references
Code:
Types and variables
Code:
Classes and inheritance
Code:
Overloading
Code:
High order functions
and decorators
A TaintMode for Python via a Library
Slides
Code:
Library
Code:
Example of primitive
untrusted
Code:
Example of primitive
ssink
Code:
Example of primitive
cleaner
Code:
Suggestion for lunch (webpage)
Implementing Erasure using Taint Analysis
Slides
Code:
Library
Code:
Example about how to use the library to erasure credit card numbers
Code:
Example of lazy erasure
Day 4
Disjunction Category Labels (DCLabels)
Slides
Code:
Categories, DCLabels, join, meet
Code:
Privileges
LIO: a library for dynamically tracking information-flow
Slides
Code:
Example of how to use
label
Code: Example of how to use
unlabel
(
trustworthy
,
untrustworthy
)
Code: Example of label creeping (
trustworthy
,
untrustworthy
)
Code: Example of how to use
toLabeled
(
trustworthy
,
untrustworthy
)
Code: Example of how to use refereces (
trustworthy
,
untrustworthy
)
Day 5
Proof of soundness for LIO
Slides
Secure Multi-Execution in Haskell
Slides
Code:
Calculator
Last modified: Saturday, 23-Jul-2011 22:42:37 CEST
COMPUTER SCIENCE AND ENGINEERING - Chalmers University of Technology and Göteborg University
SE-412 96 Göteborg, Sweden - Tel: +46 (0)31- 772 1000