Syllabus

Rationale. It is now an almost daily news story that there was yet another breakdown in cybersecurity, typically resulting from some software failure to prevent a malicious breach or an accidental misuse of publicly accessible data centers and other software systems in cyberspace – invariably with catastrophic consequences (theft of millions of passwords, loss of hundreds of millions of personal data, hacking of power grids and other critical infrastructures, etc.). Building secure and safe software is the first and most important line of defense against threats to cyberspace. Cybersecurity is a wide-ranging field, spanning human factors, hardware design, legal issues, and – most critically – software engineering. This course focuses on this final area, with the specific goal of introducing Master’s level students to the theory and use of automated tools for the production and certification of secure and safe software. Successful completion of the course will enable students to use modern methodologies and state-of-the-art automated tools to build up defenses against cyber attacks.

Topics. Students will be introduced to a variety of formal methodologies for formal specification, testing and verification, and how these can be used to understand and eliminate software bugs that undermine system security. The class will focus on two types of methodologies, dynamic and static. Dynamic methodologies include the basics of property-based testing and symbolic execution. Static methodologies include program-based formal specification and verification techniques. All these methodologies will be introduced by means of practical, industrial strength tools.

Automated tools. Students will learn the use of several automated tools and frameworks: Python with PyUnit (unit testing) and PyTest (property-based testing); OCaml with OUnit (unit testing) and QCheck (property-based testing); Dafny (formal specification and verification); Z3 and its Python API Z3Py (SAT snd SMT solver).

Prerequisites. There are two prerequisites:

• a Bachelor’s degree in computer science or in computer engineering, and

• a working familiarity with at least one modern programming language.

If either of these two requirements is not satisfied (or both), a student wishing to enroll for the course will have to talk to the course instructors and get their consent.

Course materials and documents. These will be posted on the Piazza website for the course and made available for download as the semester progresses. Reading material will consist of handouts written by the course instructors together with selected articles from the published literature on topics covered during the semester.

Course evaluation. Student performance will be based on:

• 14 weekly assignments, with each assignment to be completed and submitted electronically within one week.

Students may opt to work on assignments in pairs, where each pair will submit a single joint solution to a given assignment.

Letter grades will correspond to the following percentages of accumulated points:

• A = 90% and above,

• B = from 80% to 89%,

• C = from 70% to 79%,

• D = from 60% to 69%,

• F = 59% and below.

Final letter grades will be modified with a "+" or a "-" following standard practice of dealing with borderline cases, e.g., adding a "+" to a borderline-grade of a student who demonstrated diligence and steady improvement over the semester.

This will be a fast-pace course, and homework assignments submitted after their one-week deadline will not be graded. In the event of serious illness, make-up examinations will be given orally. There will be no "Incomplete" grades in this course.

Online discussion. We will use Piazza for announcements, queries from students to the teaching staff, and queries between students. You will get an email from Piazza with a link inviting you to create an account within the first week of the Fall 2021 semester.

Academic Conduct

Please read carefully Boston University's policies on academic conduct:

• College of Arts & Sciences policy.

• Graduate School of Arts & Sciences policy.

Instructors are required to strictly enforce these policies.