Software Security 2020/2021

Lucas Cordeiro will teach this course for post-graduate students in Computer Science and Engineering. This page contains information about the course.

Overview

Software is subject to numerous forms of attack such as memory corruption, buffer overflows and injection; these flaws are often too complex or expressive to be manually detected by the software developer. Techniques and tools exist to prevent and detect software flaws, which are typically too hard to be manually found, e.g., modelling, code reviews, fuzzing, static and dynamic code analyses, program verification and code tainting.

This course unit introduces students to basic and advanced approaches to formally build verified trustworthy software systems, where trustworthy comprise five attributes: reliability, availability, safety, resilience and security.

Relationship to other courses

Software Security involves people and practices, to build software systems to ensure confidentiality, integrity and availability. Therefore, this course has connections to other disciplines: cyber-security, cryptography, automated reasoning and verification, logic and modelling, agile and test-driven development, software engineering concepts and systems governance.

Prerequisites

Fundamental programming skills, including familiarity with C and Python 3. In more detail:

Basic notions in Linux System Administration:

Some interest/knowledge of logic and modelling:

Syllabus

Intended Learning Outcomes (ILOs)

On successful completion of this course unit, a student will be able to

MSc theme on software security and automated reasoning

You can find the slides we presented in the welcome week about our MSc theme on software security and automated reasoning.

Lectures & extra material

Lectures will be available here through slides, videos and reading materials.

Date Video Extra Content
Week 1

All videos: Introduction to Software Security

Video 1: Welcome to COMP63342

Video 2: Standard notions of security

Video 3: Software Security Problems

Video 4: Software Testing and Verification - Part I

Video 5: Software Testing and Verification - Part II

Video 6: Kripke Structure

Video 7: Synchronous Session

Slides

Coursework

Quiz

Week 2

All videos: Secure C Programming: Memory Management

Video 1: Risk Assessment

Video 2: Dynamic Data Structures

Video 3: Secure C Coding

Video 4: Data Structure Alignment

Video 5: A Static Analysis Tool for Finding Security Vulnerabilities

Video 6: Synchronous Session

Slides

Coursework

Quiz

Week 3

All videos: Detection of Software Vulnerabilities: Static Analysis (Part I)

Video 1:Introduce software verification and validation

Video 2: Understand soundness and completeness concerning detection techniques

Video 3: Emphasize the difference between static analysis, testing / simulation, and debugging

Video 4: SAT and SMT solving

Video 5: Bounded Model Checking of Software

Video 6: Memory Model

Video 7: Aligned Memory Model

Video 8: Bonus Material About SMT Floating-Point Theory

Video 9: Synchronous Session

Slides

Coursework

Quiz

Week 4

All videos: Detection of Software Vulnerabilities: Static Analysis (Part II)

Video 1: BMC Architectures

Video 2: Communication models for concurrent programs

Video 3: Lazy exploration of multi-threaded programs

Video 4: Schedule recoding approach

Video 5: Sequentialisation methods

Video 6: Bonus Material About SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

Video 7: Synchronous Session

Slides

Coursework

Quiz

Week 5

All videos: Detection of Software Vulnerabilities: Dynamic Analysis

Video 1: Introduction to security testing

Video 2: Code coverage

Video 3: Monitor Program's Executions

Video 4: Generate executions of the program

Video 5: Black-box fuzzing

Video 6: White-box fuzzing

Video 7: Bonus Material About FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs

Video 8: Synchronous Session

Video 9: Synchronous Session

Slides

Coursework

Quiz

Topics for the seminar

We provide some suggestions for software security topics for the seminars here.

Teaching Activities

Assessment

The full course will be assessed as follows:

Resources

References

The books used by this course are:

Software

The software used by this course are:

Useful Links