The goal of the course project is to produce a research paper suitable
for publication in a workshop or conference forum. Students are to work
together in small groups (2 or 3 people).
- Form groups and meet with Steve by Friday, Feb. 7th.
- Submit a one-two page writeup of related work by Feb. 21.
- Submit a one-two page introduction and motivation section of
the paper by March 7th.
- Submit a technical description of the project by April 16.
- Submit the completed project paper, including summary and contributions
by the end of the semester.
- Presentations given in the last week of class.
The projects will be graded based on the writeup at each phase, the quality
of the project technically, and the resulting final paper. Writeups are
expected to require revision and editing throughout the semester; feedback
on writing style and content will be provided. Furthermore, each group
will be encouraged to peer review the other groups' submissions at each
step of the project.
- Use Myer's Polyglot framework to implement an interesting, security-relevant
variant of Java. One idea might be to allow a class definition to include
protocol information about how its methods should be called. The compiler
would compile the extended language into Java, inserting the dynamic
checks where necessary.
- Use Cyclone, Jif, Vault, TAL, or some other research language to implement
an interesting security-related system. Example systems might be firewalls
or web browsers.
- Design a policy language that formally accounts for extensions to
the decentralized label model. Work out the theory of the policy language
and implement it in Jif. Interesting extensions include dynamic principals
and parameterized security labels.
- Cryptographic programming in Jif: Design an interface to a cryptographic
library using Jif's decentralized label model. Use the resulting library
to implement the cryptographic protocols used in a secure client-server
Sample outline for the paper
associated with suggestion 4:
Cryptographic Programming in Jif
- 1. Motivation (argument that makes the contributions seem inevitable!)
- Information security is important.
- Cryptographic primitives are crucial for network-based security.
- Language-based security is practical way to increase confidence
- Current support for cryptographic primitives in languages is not
- 2. Contributions
- Design of a cryptographic library in Jif
- Type system encodes desirable invariants
- Investigation of event driven vs. threaded programs with information
- Implementation of a (reasonably) substantial system using Jif
- Jif and Decentralized Label Model
- Important features (label abstraction, first-class principals,
- Syntax and meaning
- Cryptographic operations
- Shared vs. Public key cryptosystems
- Design of the Cryptographic Library
- Keeping keys secret
- Dependency between keys and encrypted values
- Authentication information encoded in the types
- Integrity Constraints in Jif
- Dynamic Principals
- Label polymorphism
- Fancy programming
- Evaluation of the Library
- Description of the test case
- Bank/ATM simulation with interesting authentication protocols
- Taken from CSE331 course implementation
- Implementation details/examples
- Insights learned?
- Related Work
- - Jif
- Sumii and Pierce, Cryptographic Lambda Calculus
- Smith & Volpano, Verifying Secrets and Relative Security
- Zdancewic & Myers, Robust Declassification
- Abadi & ?, ...Relating Black Box Cryptography to ...
- RSA, Protocols stuff
- Cryptyc, Spi (Gordon, Jeffries, Abadi)
- Summarize introduction
- Reiterate contributions