FCS on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program

Sessions take place in auditorium 5 unless otherwise indicated.

Session 5: FCS Invited talk

Joint with VERIFY
Room: auditorium 6
Chair: Iliano Cervesato

09:00-10:30  Dieter Gollmann, Microsoft Research Cambridge, UK
Invited talk: Defining security is difficult and error prone
It is often claimed that the design of security protocols is difficult and error prone, with formal verification suggested as the recommended remedy. Verification requires a formal statement of the desired security properties and, maybe surprisingly, many protocols are broken simply by varying the assumptions on goals and intended environment. To defend my claim that defining security is difficult and error prone (and the really interesting challenge in formal verification) I will discuss some old and new examples of security protocols and their formal analysis.

Session 6: Programming Language Security

Chair: Ernie Cohen

11:00-11:30  Lujo Bauer, Princeton U, USA
Jarred Ligatti, Princeton U, USA
David Walker, Princeton U, USA
More enforceable security policies
We analyze the space of security policies that can be enforced by monitoring programs at runtime. Our program "monitors" are automata that examine the sequence the program actions and transform the sequence when it deviates from the specified policy. The simplest such automaton truncates the action sequence by terminating a program. Such automata are commonly known as "security automata," and they enforce Schneider's EM class of security policies. We define automata with more powerful transformational abilities, including the ability to insert a sequence of actions into the event stream and to suppress actions in the event stream without terminating the program. We give a set-theoretic characterization of the policies these new automata are able to enforce and show that they are a superset of the EM policies.

11:30-12:00  Yu David Liu, Johns Hopkins U, USA
Scott F. Smith, Johns Hopkins U, USA
A component security infrastructure
This paper defines a security infrastructure for access control at the component level of programming language design. Distributed components are an ideal place to define and enforce significant security policies, because components are large entities that often define the political boundaries of computation. Also, rather than building a security infrastructure from scratch, we build on a standard one, the SDSI/SPKI security architecture.

12:00-12:30  Christian Skalka, Johns Hopkins U, USA
Scott F. Smith, Johns Hopkins U, USA
Static use-based object confinement
The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A use-based approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type soundness result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.

Session 7

Joint with VERIFY
Room: auditorium 6
Chair: Serge Autexier, Iliano Cervesato, Heiko Mantel

14:00-15:30  Ernie Cohen, Microsoft Research Cambridge, UK
Alan Jeffrey, DePaul U, USA
Fabio Martinelli, CNR Pisa, Italy
Fabio Massacci, U Trento, Italy
Catherine Meadows, Naval Research Laboratory, USA
David Basin, U Freiburg, Germany
Panel: The future of protocol verification
This panel is aimed at assessing the state of the art and exploring trends and emerging issues in computer security in general and protocol verification in particular. It brings together experts from both the security community and the verification area. Some of questions over which they will be invited to discuss their views, and maybe even to answer, include: What is already solved? What still needs improvement? What are the challenging open problems? What is the role of automated theorem proving in protocol verification? What else is there in computer security besides protocol verification? A format for this panel has been chosen as to achieve an interesting, vibrant, and productive discussion.

15:30-15:40  Closing Remarks