1.
Syllabus
❱
1.1.
Administrative Information
1.2.
Course Schedule
1.3.
Class Prep
1.4.
Programming Assignments
1.5.
Course Project
1.6.
Paper Discussion
1.7.
Approval Instructions
2.
Week 1: Rust
❱
2.1.
System Setup
2.2.
Basic Syntax of Rust
2.3.
Safety Features of Rust
2.4.
Expressive Power and Unsafe Rust
2.5.
More on Struct and Traits
3.
Week 2: Rust (Continued)
❱
3.1.
Lifetimes
3.2.
?, dyn, and Macros
3.3.
Useful Crates and Tools
3.4.
Idioms and Design Patterns
❱
3.4.1.
Use Expressions
3.4.2.
Use Pattern Matching and Destructuring
3.4.3.
Use Iterators
3.4.4.
Avoid Declaring First
3.4.5.
Think About clone() Before Using It
3.4.6.
Use the Debug Formatter
3.4.7.
Use #[derive()]
3.4.8.
Implement the Display Trait
3.4.9.
Implement new()
3.4.10.
Implement the Default Trait Along with new()
3.4.11.
match De-Nesting
3.4.12.
Processing Collections of Items Using Functional Language Features
3.4.13.
Use Method Chaining
3.4.14.
Error Handling
3.4.15.
New Type Idiom
3.4.16.
Use &str, &T, and &[T] for Function Parameters
4.
Week 3: Fuzz Testing, Property-Based Testing, Symbolic Execution, and SAT/SMT
5.
Week 5: Rust analyses
6.
Week 6: Rust OSes
7.
Week 7: Symbolic Execution
8.
Week 8: Hybrid Fuzzing
9.
Week 9: Formal Methods
10.
Week 10: Formal Methods (Continued)
11.
Week 11: Interactive Verification
12.
Week 12: Automated Verification
Light (default)
Rust
Coal
Navy
Ayu
CMPT 479/982
Course Schedule
The following schedule is subject to change.
Week
(Date)
Discussion
Class Prep
Due
Week 1 (Sep 8)
Course Introduction &
Rust
Week 2 (Sep 15)
Rust (continued)
&
How to Read a Paper
-
The Rust Book
up to Chapter 11
-
Rust by Example
-
Rust Design Patterns
-
How to Read a Paper
Milestone 1: Team Formation
Week 3 (Sep 22)
Fuzz Testing
,
Property-Based Testing
,
Symbolic Execution
, and
SAT/SMT
-
An Empirical Study of the Reliability of UNIX Utilities
-
QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs
-
Symbolic Execution and Program Testing
-
Problem Solving for the 21st Century
Milestone 2: Topic Selection
Week 4 (Sep 29)
Class canceled
Week 5 (Oct 6)
Rust Analyses
-
The Usability of Ownership
-
How Do Programmers Use Unsafe Rust
Programming Assignment 1
Milestone 3: Problem Selection & Proposal
Week 6 (Oct 13)
Rust OSes
(Cars in Space)
-
RedLeaf: Towards An Operating System for Safe and Verified Firmware
-
Theseus: an Experiment in Operating System Structure and State Management
Week 7 (Oct 20)
Symbolic Execution
(Black Diamond)
-
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
-
Verifying Dynamic Trait Objects in Rust
Week 8 (Oct 27)
Hybrid Fuzzing
(Rusting Away)
-
Driller: Augmenting Fuzzing Through Selective Symbolic Execution
-
HFL: Hybrid Fuzzing on the Linux Kernel
Week 9 (Nov 3)
Formal Methods
Week 10 (Nov 10)
Formal Methods (Continued)
-
How Amazon Web Services Uses Formal Methods
-
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
Milestone 4: Intermediate Demo
Week 11 (Nov 17)
Interactive Verification
(Lionfish)
-
seL4: Formal Verification of an OS Kernel
-
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
Programming Assignment 2
Week 12 (Nov 24)
Automated Verification
(In the Loop)
-
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
-
A Formally Verified NAT
Week 13 (Dec 1)
Project Demos and Presentations
Milestone 5: Final Demo & Report