CSE590 Section 1
High-Assurance Software Design and Implementation

Course Information

Semester:	Spring 2023
Time:	Monday and Wednesday, 11:30 AM - 12:50 PM
Class Location:	Old Computer Science Building, Room # 2311
Credits:	3 Credit Hours
Prerequisites:	This is a graduate special topics course and does not have any prerequisites.
Textbooks:	The class does not require any textbook. The instructor will make PowerPoint/PDF slides available to the student covering different relevant topics through Piazza. We will also consult relevant research papers that will be made available through Piazza. Students are encouraged to discuss the course material and challenges they face in solving the assigned homework. For group discussions, we will use Piazza. Prior to asking questions, as a courtesy to the instructor and the TA, the students are advised to make sure that their questions have not been previously answered.

Contact Information

Instructor:	Omar Haider Chowdhury, Ph.D.
Email:	omar@cs.stonybrook.edu
Office hours:	Tuesday, 10:00 AM - 11:30 AM, Wednesday, 3:00 PM - 4:30 PM, and by appointment.
Office location:	New Computer Science Building Room 363 (NCS 363)
Teaching Assistant:	Joyanta Debnath, Ph.D. Student
Email:	jdebnath@cs.stonybrook.edu
Office hours:	Monday, 3:00 PM - 4:30 PM, Thursday, 10:00 AM - 11:30 AM, and by appointment.
Zoom Link:	https://stonybrook.zoom.us/j/4835889823?pwd=YURGakhQY2lZS1o4UjhNTkZKQ3lhZz09

Course Overview

This class will introduce the students to applying automated reasoning approaches (e.g., model checking, runtime monitoring, auditing, cryptographic protocol verification, SMT, SAT, program analysis, symbolic execution) for detecting and proving the absence of security and privacy vulnerabilities of emerging systems, software, and protocols. The covered topics include (but not limited to):

SMT/SAT and its application to analyzing security and privacy policies and bounded model checking of software.
Symbolic execution and its application to finding vulnerabilities in system, software, and protocol (e.g., TLS, X.509).
Program analysis (e.g., data flow, control flow, taint analysis) for detecting vulnerabilities in systems, software, and protocols (e.g., Android, Augment Reality, Internet-of-Things).
Model checking and its application to analyzing the compliance of protocols (e.g., 4G LTE, Bluetooth).
Runtime monitoring, auditing, and their applications to checking compliance with privacy policies (e.g., HIPAA, GLBA).
Cryptographic protocol verification and its applications to proving the security of cryptographic protocols (e.g., authenticated key exchange).
Advanced topics (e.g., cryptocurrency, smart contracts, program synthesis, CEGIS)

Course Objectives

After the successful completion of this course, a student will be able to achieve the following objectives:

An understanding of C-style software vulnerabilities such as buffer overflow and integer overflow.
An understanding of basic automated reasoning techniques such as SAT, SMT, and Model Checking.
An ability to identify automated reasoning techniques to apply on a software security problem.

Resources

Software and Reasoning Engines

Tutorial and Documentation

OCaml Programming Web book
The official SMT-LIB Documentation
SMT Background Materials
SMT Tutorial from Microsoft
SMT Tutorial at Stanford
NuSMV Model Checker User Manual
NuSMV Model Checker Tutorial
KLEE Symbolic Execution Tutorial
Dafny Reference Manual
Tamarin Documentation

Course Schedule

Date	Topic	Summary/Notes
01/23/2023	Introduction and administrative stuff	See Piazza for Lectures
01/25/2023	Software Security 1	See Piazza for Lectures
01/30/2023	Software Security 2, 3, 4	See Piazza for Lectures
02/01/2023	Software Security 5, 6	See Piazza for Lectures
02/06/2023	Introduction to Automated Reasoning + Introduction to Propositional Logic	See Piazza for Lectures + HW1 out (Individual Paper Reading Assignment)
02/08/2023	SAT Solving + Applications to SAT Solving	On the Security and Usability of Segment-based Visual Cryptographic Authentication Protocols
02/13/2023	Applications of SAT Solving + Introduction to SMT
02/15/2023	Internals of SMT Solving + Introduction to theory combination	HW1 DUE. HW2 OUT. (OCaml Problems)
02/20/2023	Theory Combinations in SMT
02/22/2023	Introduction to Symbolic Execution	HW2 DUE. HW3 OUT. (Writing a DPLL SAT Solver)
02/27/2023	Applications of Symbolic Execution
03/01/2023		Midterm Exam 1
03/06/2023	Introduction to Temporal Logic; Safety and Liveness Properties	HW3 DUE. HW4 OUT. (Writing an interpreter for a simple imperative programming language in OCaml)
03/08/2023	Introduction to Model Checking
03/13/2023 - 03/19/2023	Spring Break
03/20/2023	Hands-on Experience with a Model Checker	HW4 DUE. HW5 (Application of SMT Solving) OUT Final Programming Assignment OUT (Writing Symbolic Execution and Taint Tracking Engines for a simple imperative language --- extension of HW4)
03/22/2023	Introduction to Program Verification and Hoare Logic
03/27/2023	Program Verification (Continued)	HW5 DUE. HW6 OUT. (Using Model Checking for solving security problem)
03/29/2023	Non-interference and Non-deducibility; Hyperproperties
04/03/2023	Introduction to Taint Tracking
04/05/2023	Taint Tracking (Continued)	HW6 DUE
04/10/2023	Runtime Monitoring of Linear Temporal Logic
04/12/2023	Introduction to Language and Automata
04/17/2023	Introduction to Black-box Automata Learning
04/19/2023	Applications of Black-box Automata Learning
04/24/2023	Basics of Cryptography (Symmetric and Assymetric Key Cryptography)
04/26/2023		Midterm Exam 2
05/02/2023	Hands-on Experience with Cryptographic Protocol Verification
05/04/2023	Application of Combining Model Checking and Cryptographic Protocol Verification
05/08/2023 - 05/17/2023	Final Examination Week	Final Programming Project Due

Grading Policies

Grading

Exams will be comprehensive, covering everything up to the exam date, emphasizing integrating material from recent assignments. Exam may include both multiple- choice, numerical problems, and understanding/writing snippets of code. Each midterm exam will take place in-class. Students that cannot attend the exam due to conflicts (e.g., illness, religious holidays) may make alternate arrangements (in advance, if at all possible). For the programming assignments, student will be required to use a functional programming language likely OCaml. The students will be notified of other automated reasoning engines or libraries necessary for finishing a homework assignment. Programming assignments will be the hardest part of the class. Students are encouraged to start early. A software program will automatically check for cheating in all student submissions. Cheating will not be tolerated and will results in a grade of zero for that assignment. Students are requested to consult the instructor to ensure whether collaboration is allowed in particular assignments. The students may also be asked to review some current research papers (shared via Piazza) on relevant topics. Paper reading assignments may ask students to write a generic summary of the paper as well as require them to answer specific questions.

The following is a tentative distribution of the grades and may change in the middle of the semester.

Homework assignments, including written and programming assignments, will contribute to the 70% of the course grade.
Midterm examination 1 will contribute to the 15% of the course grade.
Midterm examination 2 will contribute to the 15% of the course grade.
There is no final examination for this class.

Late and Incomplete Work

Each student will be entitled to 3 late days in total over the whole semester. One late day may be used to delay the homework or programming project submission for a single day. A student can use all the 3 late days for a single homework or programming project submission. Note that, late submissions for which students have no late days available will not be accepted. Students should exercise the late days wisely. Grades will be assigned based on individual merit and performance in class. The instructor will assign A+ only to students who perform excellent in class. Otherwise, a grade without +/- will be assigned.

Make-up Exam Policy

Do not miss any exams. Make-up exams will be given only in extenuating circumstances (e.g., doctor's note stating that you were ill and unfit to take the exam). Students who miss an exam for a valid reason must contact the instructor immediately to take a make-up exam at the earliest possible time; specific arrangements will be made on a case-by-case basis.

Other Logistics

Emergency Evacuation

Students who require assistance during emergency evacuation are encouraged to discuss their needs with their professors and the Student Accessibility Support Center. For procedures and information go to the following website and search Fire Safety and Evacuation and Disabilities.

Student Accessibility Support Center Statement

If you have a physical, psychological, medical, or learning disability that may impact your course work, please contact the Student Accessibility Support Center, Stony Brook Union Suite 107, (631) 632-6748, or at sasc@stonybrook.edu. They will determine with you what accommodations are necessary and appropriate. All information and documentation is confidential.

Academic Integrity Statement

Each student must pursue his or her academic goals honestly and be personally accountable for all submitted work. Representing another person's work as your own is always wrong. Faculty is required to report any suspected instances of academic dishonesty to the Academic Judiciary. Faculty in the Health Sciences Center (School of Health Professions, Nursing, Social Welfare, Dental Medicine) and School of Medicine are required to follow their school-specific procedures. For more comprehensive information on academic integrity, including categories of academic dishonesty please refer to the academic judiciary website.

Critical Incident Management

Stony Brook University expects students to respect the rights, privileges, and property of other people. Faculty are required to report to the Office of Student Conduct and Community Standards any disruptive behavior that interrupts their ability to teach, compromises the safety of the learning environment, or inhibits students' ability to learn. Faculty in the HSC Schools and the School of Medicine are required to follow their school-specific procedures. Further information about most academic matters can be found in the Undergraduate Bulletin, the Undergraduate Class Schedule, and the Faculty-Employee Handbook.

CSE590 Section 1 High-Assurance Software Design and Implementation