| |
Are there general principles underlying the design of secure systems? This series of lectures
will consider this question and its historical answers. More specifically, we will look at the
principles of complete meidation, least priviledge, minimizing the trusted computing
base, security as process, economy of mechanism, etc. The lectures will draw on examples
from real systems and current research with the intent of setting the stage for the rest of the
summer school.
The security technology developed by engineers and computer scientists has little chance at being
effictice unless surrounding legal, economic and societal concerns are considered. We will teach
students how to think about the larger issues and incorporate them in their research. More
specifically, we will study:
- Security and incentives: The security choices made by vendors and consumers are influenced by
market forces. Do market incentives lead to good security choices? How might legal changes, such as a
shift in liability rules, affect the stakeholders' choices.
- Surveillance and privacy: New technologies allow small recording devices to be deployed widely.
This raises obvious privacy concenrs. How do these technologies affect personal privacy? How might
technology help to mitigate these privacy concerns? How should we balance the needs of law
enforcement with citizens' rights and expectations?
Access control is central to security in computer systems. Over the years, there have been many
efforts to explain and to improve access control, somethimes with logical ideas and tools. These
lectures are a partial survey and discussion of the role of logic in access control. They consider
logical foundatons for access control and their applications, in particular in langugages for
programming security policies. Although logic is not a panacea, its applictions in access control have
been substantial and beneficial.
We will introduce type systems, the most basic mechamism for static verification of program behavior.
Students will learn how to define type systems for simple programming languages and how to prove that
their type systems are sound. The focus in this introductory set of lectures will be on safety for
functional languages. These lectures serve as introductory material for the more advanced topics on
type checking and static safety.
|
|
