CIS700: Formal Methods in Computer Security

Syracuse University ECS. Fall, 2020

Professor:
Kristopher Micinski <kkmicins@syr.edu>

Please join the class slack channel!

The goal of this course is to help students develop research maturity in areas at the intersection of formal methods and computer security. The course will survey relevant foundations of formal methods (logics, model checking, etc...) and contextualize their relevance to defining and reasoning about the security of computational systems. We will mainly do this by reading and discussing research papers in these areas.

The course will contain several individual assignments / programming projects. These projects will be open-ended in nature: a functional specification will be given but students will write (or code) up solutions individually (the instructor may occasionally provide starter code). There will also be a final project wherein students explore an incremental research problem relevant to the course.

Grading information can be found under the "Grading" section.

Projects

The first half of the course will consist of four projects taking roughly two weeks each. Projects will have students implement ideas from class as programming exercises. A time investment of around three to to eight hours per week outside of class is expected on these projects.

Projects will be announced here as they are scheduled.

Readings and Comments

Important note: reading discussion takes place under the "Discussions" tab in the course’s Blackboard (blackboard.syr.edu).

This course will involve reading and discussing (in class) a corpus of research papers at the intersection of formal methods and security. After reading each paper, students will complete a graded "journal entry" consisting of a two-paragraph reflection that summarizes the core ideas, problems, and insights contained in each reading. Students will also be asked to generate several discussion questions for the class. Journal entries will be due 24 hours in advance of paper discussions, and students will be expected to have skimmed each others’ journal entries before discussing the paper in class.