Security by Design is a software development approach that integrates security tactics and patterns from the beginning of software design to build security into the system from the ground up. Formal methods for software specification and verification are a host of mathematical techniques and tools that can support the design and development of secure systems following the security by design approach.
This course provides a high-level introduction to security by design using formal methods, including case studies and experience reports from industry. The fundamentals of this approach are illustrated using industry-level tools for formal software specification like TLA+ and its toolbox for model-checking and machine-checked proofs.
In the course you will go through the following elements:
Principles of Security by Design.
Basic elements of formal methods for software specification and verification.
Examples and case studies using TLA+ or similar industry-level tools.
With the course you will be able to:
Describe the principles of Security by Design, their motivation, impact, and common tradeoffs.
Identify the relevant advantages and disadvantages of using different suites of formal methods in a software project.
Develop small projects using formal specification tools.
Programmers, Software Architects, Product Managers, and Technology/Innovation Officers with some development experience.
Assistant Professor Marco Peressotti is on a research mission to make it more effective and robust to program and analyse concurrent systems. An overarching theme of his research approach is the use of formal methods and programming languages techniques as well as the aim for a unifying mathematical perspective rooted in Logic and Category Theory.