Language-Based Security 2023

Organization

• Instructor: Aslan Askarov
• Location: 5520-112
• TA: in my dreams

Course Plan

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

Feb 3rd

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.

Assignment:

• Warm up (programming assignment)

Feb 10th

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
  1. Abadi et al.
• Bonus: SoK: Eternal War in Memory by Szekeres et al.

Assignment:

• Basic buffer overflows (programming assignment)

Feb 17th

Capabilities: principles and object capability model {slides}

Reading:

• Sections 1 - 3 of Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code by Georges et al.
• The Confused Deputy: (or why capabilities might have been invented) by
  1. Hardy.
• Chapters 8 and 9 of M. Miller's thesis Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control.

Bonus reading:

• The CHERI capability model: Revisiting RISC in an age of risk
• Joe-E: A Security-Oriented Subset of Java
• seL4: Formal Verification of an OS Kernel

Assignment:

• Object Capabilities (theoretical assignment)

Feb 24th

Capbiility machines. {slides}

Execution Monitoring {slides}

Reading:

• Enforceable Security Policies

Bonus:

• Efficient Software-Based Fault Isolation
• IRM Enforcement of Java Stack Inspection

Assignment:

• Capabilities (theoretical assignment)

Mar 3rd

Introduction to information flow.

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

Mar 10th

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:

• Info flow (theoretical assignment)

Mar 17th

Troupe

Assignment:

• Info flow (programming assignment)

Mar 24th

No lecture

Mar 31st

Quntitative security

Overview of the papers and project ideas

Apr 14th

TBD

Apr 21st

TBD

Apr 28th

<student paper presentations>

May 12th

<student paper presentations>

May 19th

<student paper presentations>

Wrap up