Language-based Security Tutorial

Schedule and Topics

Tutorial 18.10.2006 Tutorial 25.10.2006 Tutorial 08.11.2006 Tutorial 15.11.2006 Tutorial 22.11.2006 Tutorial 29.11.2006 Tutorial 06.12.2006

Tutorial 13.12.2006 Tutorial 20.12.2006 Tutorial 10.01.2007 Tutorial 17.01.2007 Tutorial 24.01.2007 Tutorial 31.01.2007 Tutorial 14.02.2007

My Office Hour
Tuesday 10:00 – 11:00, Building E1.1, Room U18

Details
Here are some details about the Language-based Security tutorial (the authoritative source of information remains the website of the lecture). The tutorial takes place every Wednesday from 9:15 to 10:45 (the lecture is given immediately afterwards – 11:15 to 12:45), and every second week we have a 20 minutes quiz. The quizzes count for 30% of the final grade, and the worst graded quiz is not considered for the final grade. An average of 50% in the quizzes is required to be accepted in the final exam.

Note
One more thing which is not very common around here is that tutorials start on the first week. Immediately after the first lecture, we will do very basic things related to the lambda calculus and operational semantics. Things like the inductive definitions of terms and derivations, recursively defined functions, structural recursion on terms and derivations. We will also gain more intuition and try out examples about the basics of lambda calculus (concrete vs abstract syntax, capture-avoiding substitutions, values, stuckness, divergence). Sure, many won’t need this kind of introduction, but remember that tutorials are optional (unless there is a quiz). And I think it will be very useful for those who have never seen a lambda in their whole life.

Additional Reading (To be extended)
These are just papers I enjoyed reading while preparing for this tutorial. They are not reading material required for this lecture.

Introduction

• Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing. 2000

Type Systems

• Luca Cardelli. Type Systems. 1997

Information-flow Security

• Lantian Zheng, Andrew C. Myers. Dynamic Security Labels and Noninterference. 2004.
• François Pottier and Vincent Simonet. Information Flow Inference for ML. 2003
• Andrei Sabelfeld and David Sands. A Per Model of Secure Information Flow in Sequential Programs. 2001.

Typed Assembly Language

• Gred Morrisett and David Walker. From System F to Typed Assembly Language. 1999
• Greg Morrisett, et. all. Stack-Based Typed Assembly Language. 2002.
• Nick Benton. A Typed, Compositional Logic for a Stack-Based Abstract Machine. 2005.

Proof-carrying code

• Benjamin Pierce. Chapter 5 of Advanced Topics in Types and Programming Languages. 2005.
• George C. Necula, et all. A Certifying Compiler for Java. 2000

Practical Stuff

• Aleph One. Smashing The Stack For Fun And Profit.
• Gred Morrisett, et all. Cyclone: A Type-Safe Dialect of C. 2004

Implementations

• Cyclone
• TALx86