FOSAD 2009 Programme
The school alternates monographic courses of 4 hours each.
Timetable: download as a pdf
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
A Foundation for Verifying Concurrent Programs
Part 0 -
Part 1 -
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.
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
Part 1 - Part 2
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.
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.
Resource Usage Analysis and its Application to Resource Certification
Part 1 - Part 2
Resource usage is one of the most important characteristics of
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.
Trust Based Authorization, Independence and Monoculture
Ref.: 1 and
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.
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.