Logically Well-Founded Approaches to Computer Security
Computer security is a central issue of 21st century technology and society. Correct design of robust security systems is essential, since errors can be disastrous. But what is "correct" design, and how is it enforced? Logically well-founded approaches to computer security seek to ground systems design in mathematical logic, providing designers with a sound, consistent, and expressive system semantics. This allows a precise characterization of security properties, as well as a formal setting for proving that security properties are enforced.
In this presentation we will discuss the nature and benefits of logically well-founded security systems design. The discussion will be illustrated by two particular examples of practical interest: type safety for programming language-based security mechanisms, and efficient and reliable authorization architectures for web services.