Language-Based Security 2025

Organization

• Instructor: Aslan Askarov
• Location: 5335-192
• TA: June Rousseau

Course Plan

The schedule is tentative all term. Please stay tuned for updates.

Jan 29

Introduction. Principles of security. {slides}

Reading:

• Section 1 of The Protection of Information in Computer Systems by J. Saltzer and M. Schroeder.
• A note on the confinement problem by B.Lampson.
• Reflections on trusting trust by K.Thompson.
• The Research Value of Publishing Attacks by D. Basin and S. Capkun.

Assignment:

• Warm up (programming assignment)

Feb 5

Memory safety: Buffer overflows, Return-oriented programming, ASLR, Control Flow Integrity. {slides}

Reading:

• Smashing the stack for fun and profit by Aleph One.
• Return-oriented programming by R. Roemer, E. Buchanan, H. Shacham and S. Savage.
• On the effectiveness of address-space randomization by H. Shacham et al.
• Control Flow Integrity Principles, Implementations, and Applications by M. Abadi et al.
• Back to the building blocks: a path toward secure and measurable software. White House ONCD report, 2024
• Bonus: SoK: Eternal War in Memory by Szekeres et al.

Assignment:

• Basic buffer overflows (programming assignment)

Feb 12

Capabilities: principles and object capability model {slides}

Reading:

• The Confused Deputy: (or why capabilities might have been invented) by N. Hardy.
• Chapters 8 and 9 of M. Miller's thesis Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control.
• Joe-E: A Security-Oriented Subset of Java

Bonus reading:

• The CHERI capability model: Revisiting RISC in an age of risk
• seL4: Formal Verification of an OS Kernel

Assignment:

• Object Capabilities (theoretical assignment)

Feb 19

Capbiility machines {slides} Execution Monitoring {slides}

Reading:

• Sections 1 - 3 of Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code by Georges et al.
• Enforceable Security Policies

Bonus:

• Identifiers are not capabilities by D. Chisnall.
• Efficient Software-Based Fault Isolation
• IRM Enforcement of Java Stack Inspection

Assignment:

• Capabilities (theoretical assignment)

Feb 26

Introduction to information flow. {slides}

Reading:

• A Perspective on Information Flow Control by D. Hedin and A. Sabelfeld
• Lecture notes: Language-Based Information Flow Basics

Exercises:

• Information flow challenge
• JSFlow challenge

Assignment:

• Info flow (theoretical assignment)

Extra:

• Example implementation of the language and the type system from the lecture.

Mar 5

Information flow (cont'd). Label models

Reading:

• Sections 1 - 2 of A lattice model of secure information flow by D. Denning.
• Protecting Privacy using the Decentralized Label Model by A. C. Myers and B. Liskov.
• Bonus: Nonmalleable information flow control by E. Cecchetti et al.

Assignment: TBD

Mar 12

Troupe

Assignment:

• Info flow (programming assignment)

Mar 19

Quntitative security. {slides}

Reading:

• On the foundations of quantitative information flow

Overview of papers for presentations

Mar 26

Smart contracts. Overview of project ideas.

Apr 2

TBD

Apr 9

Guest lecture by Erik Krogh Kristensen (Github) on Autofix and CodeQL (details: TBD)

Apr 23

Paper presentations

Apr 30

Paper presentations

May 7

Paper presentations

May 14

Paper presentations. Wrap up