15-819 Languages and Logics for Security

Description

This is a graduate reading course on research topics in languages and logics for computer security. The emphasis will be on the use of methods from proof theory, type theory, and semantics to address problems in computer security. Topics include logics of authorization and information flow, type systems and program analyses for security, and the design and implementation of languages for enforcing security requirements in software systems.

The purpose of this course is to provide a technical foundation for the joint Carnegie Mellon / University of Pennsylvania project on Manifest Security.

Participation in this course consists of presenting one or more research papers. Students are expected to prepare slides that will appear on the course web page. Presentations are expected to last one course period, including discussion.

Students in this course may also be interested in Anupam Datta's course on Foundations of Security and Privacy in the ECE Department.

Schedule

Date		Presenter	Topic	References	Slides
Sep	10	Harper	Overview and Context	Manifest Security	Manifest Safety and Security
	12	Harper	Authentication Logic	A Logic of Authentication	A Logic of Authentication
	17	Datta	Protocol Composition Logic	Protocol Composition Logic (PCL)	A Logic for Security Protocols
	19	Kumar	Access Control	A Calculus for Access Control in Distributed Systems	Access Control Calculus
	24	Simmons	Authentication	Authentication in Distributed Systems: Theory and Practice	Authentication in Distributed Systems
	26	Ley-Wild	Proof-Carrying Authorization	Access Control for the Web via Proof-Carrying Authorization , Consumable Credentials in Logic-Based Access Control	Proof-Carrying Authorization
Oct	1	Gao	Distributed Authorization	Delegation Logic: A logic-based approach to distributed authorization	Delegation Logic
	3	Tschantz	Types for Authorization	A Type Discipline for Authorization Policies	Using Types to Embed Authorization Policies into Spi
	8	Garg	Constructive Authorization Logic	A Linear Logic of Authorization and Knowledge, Non-Interference in Constructive Authorization Logic	Constructive Authorization Logic
	10	(no class)
	15	(Arnab Roy)	Computational Protocol Composition Logic	Probabilistic Polynomial-Time Semantics for a Protocol Security Logic , Inductive Proofs of Computational Secrecy	Inductive Proofs of Computational Secrecy
	17	Lee	Languages for Authorization	A Core Calculus of Dependency, Access Control in a Core Calculus of Dependency	Access Control in DCC
	22	Simmons	Authentication	Authenticity by Typing for Security Protocols	Authenticity by Typing
	24	Krishnaswami	Authorization	A Monadic Analysis of Information Flow Security With Mutable State	A Monadic Language for Information Flow
	29	Ley-Wild	Information Flow	Secure Program Partitioning	Secure Program Partitioning
	31	(no class)
Nov	5	Kumar	Information Flow	On Typing Information Flow	Typing Information Flow
	7	Tschantz	Information Flow	End-to-End Availability Policies and Noninterference	End-to-End Availability Policies
	12	Kaynar	Information Flow	Enforcing Robust Declassification and Qualified Robustness	Enforcing Robust Declassification
	14	Simmons	Information Flow	Access Control and Declassification	Sanity-Checking Information Control Via Access Control
	19	Lee	Information Flow	A Cryptographic Decentralized Label Model	Cryptographic Decentralized Labels
	21	(no class)	(thanksgiving break)
	26	Garg	Calculi	Hiding Names: Private Authentication in the Applied Pi Calculus	Private Authentication
	28	(no class)
Dec	3	Gao	Calculi	Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus	Secrecy Despite Compromise
	5	Krishnaswami	Info Flow	Quantitative Information Flow, Relations, and Polymorphic Types

Time:	Mon-Wed 3:00-4:30
Room:	5409 Wean Hall
Instructor:	Robert Harper

15-819 Languages and Logics for Security

Course Information

Description

References

Schedule