CEUB FOSAD 2009 Programme

The school alternates monographic courses of 4 hours each.
Timetable: download as a pdf

Martin Abadi Logic in Access Control

Access control is central to security in computer systems. Over the years, there have been many efforts to explain and to improve access control, sometimes with logical ideas and tools. These lectures are a partial survey and discussion of the role of logic in access control. They consider logical foundations for access control and their applications.

Rustan Leino A Foundation for Verifying Concurrent Programs
Part 0 - Part 1 - Chalice Examples

These lectures focus on the correctness of concurrent programs, looking at how to specify programs that use locks to achieve fine-grained concurrency, the semantic model of such programs, and how to build an accompanying static program verifier. The specification style is based on a model of permissions. The verifier translates programsand their specifications into an intermediate verification language, from which first-order proof obligations are generated.

Javier Lopez Wireless Sensor Network Security

As sensor networks are more and more being implemented in real world settings, it is necessary to analyze how the different requirements of these real-world applications can influence the security mechanisms. This lecture offers both an overview and an analysis of the relationship between the different security threats, requirements, applications, and security technologies. Besides, it also overviews some of the existing sensor network standards, analyzing their security mechanisms.

Ueli Maurer Constructive Cryptography

Part 1 - Part 2

David Pichardie Certified Static Analysis

A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. This lecture is on building a certified static analysis in Coq. We study a simple bytecode language for which we propose an interval analysis that allows to verify statically that no array-out-of-bounds accesses will occur.

Erik Poll Specifications, Verifications and Proofs for Java

These lectures will discuss the Proof Carrying Code infrastructure for Java developed in the Mobius project, and its application to specify security aspects of Java code for mobile devices.

German Puebla Resource Usage Analysis and its Application to Resource Certification
Part 1 - Part 2

Resource usage is one of the most important characteristics of programs. Automatically generated information about resource usage can be used in multiple ways, both during program development and deployment. In this lecture we discuss and present examples on how such information is obtained in COSTA, a state of the art static analysis system. COSTA obtains safe symbolic upper bounds on the resource usage of a large class of general-purpose programs written in a mainstream programming language such as Java (bytecode). We also discuss the application of resource-usage information for code certification, whereby code not guaranteed to run within certain user-specified bounds is rejected.

Fred Schneider Trust Based Authorization, Independence and Monoculture
Ref.: 1 and 2

Ultimately, authorization should be based on the extent to which the principal making a request is trusted. We will describe a language, logic, and mechansims used for implementing this approach to authorization in the Nexus operating system and in some document-managment applications. The roles of analytic, axiomatic, and constructive bases for trust will be discussed.
Independence of replica failures is crucial when using replication for reliable distributed services. But replicas that use the same code share the same vulnerabilities. So, replicas do not fail independently when under attack. More generally, monocultures in cyberspace would seem to be exceptionally vulnerable to malware outbreaks. In this talk, we will revisit the conventional wisdom about eschewing monocultures and also discuss the role and power of artificially-induced diversity - both in foundational terms and through example distributed services that have been prototyped.

Luca Viganò On-the-fly Model Checking of Security Protocols and Web Services

In this lecture, we introduce the Open-source Fixed-point Model Checker OFMC for symbolic security protocol analysis, which extends the On-the-fly Model Checker (the previous OFMC). The native input language of OFMC is the AVISPA Intermediate Format IF. OFMC also supports AnB, a new Alice-and-Bob-style language that extends previous similar languages with support for algebraic properties of cryptographic operators and with a simple notation for different kinds of channels that can be used both as assumptions and as protocol goals.