SRL Publications Projects Courses

Courses

600.318/600.418

600.328/600.428

600.436

600.438

600.439

600.438: Advanced TOpics in Operating Systems


 
Fall 2000 Syllabus (Preliminary)  

The course will be divided into three roughly equal parts. The first segment will look at theoretical and formal foundations for protection and security in operating systems. We will look at access control models, information flow issues, and some well-known security policies. The second segment will look at sverral real systems, with an eye toward understanding some of the history and the current state of the art in secure system construction. The final segment will focus on capability systems, which appear to address some of the issues we will raise in the earlier portions of the course.

The course will hopefully involve projects based on the EROS secure nucleus (see EROS). In the event that the EROS system does not meet its expected schedule, this will be deferred in favor of a look at other issues in operating system security.

This course will be based on readings of original papers. Students are expected to read the material in advance of the associated class meeting, and to participate actively in discussion of the subject matter.

The syllabus that follows is a work in progress!

Week of Topic(s) and Papers
11 Sep 2000

Defining the Problem: The Operating System View of Security

Readings

M. Bishop. Academia and Education in Information Security: Four Years Later, Academic keynote speech to the 2000 National Colloquium on Information System Security.

Morrie Gasser. Building a Secure Computer System, Chapter 9: Security Models, Van Nostrand Reinhold, New York.

Lecture

Introductory overview of operating system security issues. How operating system security differs from the usual approaches to network and cryptographic security, and what unique problems are raised by these differences.

18 Sep 2000

Security Models

Readings

Carl E. Landwehr. "Formal Models for Computer Security." Computing Surveys. 13(3):247-278 (September 1981)

Dorothy E. Denning. "A Lattice Model of Secure Information Flow." Communications of the ACM. 19(5) (May 1976)

Butler W. Lampson. "A Note on the Confinement Problem." Communications of the ACM. 16(10) (October 1973)

Lecture

Discussion of the commonly known security models, their weaknesses and limitations. Discretionary vs. mandatory acess policies.

25 Sep 2000

Protection I: The Lampson Access Matrix and Access Control Lists

Readings

Butler Lampson. "Protection." Proc. 5th Princeton Conference on Information Sciences and Systems. Princeton, 1971, p 437. Reprinted in Operating Systems Review 8(1):18-24 (Jan. 1974)

M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. "A Calculus for Access Control in Distributed Systems." ACM Transactions on Programming Languages and Systems. 15(4):706-734. Originally DEC SRC Report #70 Feb. 28 1991, Revised Aug. 28 1991.

Michael A. Harrison and Walter L. Ruzzo. "Protection in Operating Systems." Communications of the ACM. 19(8):461-471 (August 1976)

Optional

Ravi S. Sandhu. "The Typed Access Matrix Model." Proc. IEEE Symposium on Security and Pricvacy. Oakland, CA. 1992 pp. 122-136

Ravi S. Sandhu, Edward J. Coyne, Hal L. Feinstein, andd Charles E. Youman. "Role-Based Access Control Models." IEEE Computer. 29(2):38-47 (February 1996)

Lecture

Further discussion of access models, the use and limitations of Lampson's "Access Matrix", and the problem of terminology evolution. The difference between allegation and truth in discussing security issues. Advisable, inadvisable, and invalid use of "cost based" security arguments.

2 Oct 2000

Protection II: Capabilities

Readings

Jonathan S. Shapiro. What is a Capability Anyway?

J. B. Dennis and E. van Horn. "Programming Semantics for Multiprogrammed Computation." Communications of the ACM. 9(3):143-155 (March 1966)

R. S. Fabry. "Capability-Based Addressing." Communications of the ACM. 17(7) (March 1966) p. 143

M. Bishop and L. Snyder. "The Transfer of Information and Authority in a Protection System." 7th Symposium on Operating System Principles. pp. 45-54, 1979

W. E. Boebert. "On the Inability of an Unmodified Capability Machine to Enforce the *-Property". Honeywell Systems and Research Center.

Lecture

Fill me in.

9 Oct 2000

Verification I

Readings

R. J. Lipton and L. Snyder. "A Linear Time Decidable Algorithm for Deciding Subject Security." Journal of the ACM. 24(3):455-464 (July 1977)

John Rushby. Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02. SRI International Computer Science Laboratory. December 1992.

Lecture

Fill me in.

16 Oct 2000

Mid-Term Week

Review Tuesday, October 17
Mid-Term Wednesday, October 18
23 Oct 2000

Timing and Storage Channels

Readings

John C. Wray. "An Analysis of Covert Timing Channels." 1991 IEEE Symposium on Security and Privacy, Oakland, CA. pp. 2-7

Wei-Ming Hi. "Reducing Timing Channels with Fuzzy Time." 1991 IEEE Symposium on Security and Privacy, Oakland, CA. pp. 8-20

Paul A. Karger and John C. Wray. "Storage Channels in Disk Arm Optimization." 1991 IEEE Symposium on Security and Privacy, Oakland, CA. pp. 52-61

Lecture

Fill me in.

30 Oct 2000

The VAX Security Kernel

Readings

Judith S. Hall and Paul T. Robinson. "Virtualizing the VAX Architecture." Computer Architecture News. vol. 19. pp. 380-389 (May 1991).

Paul A. Karger, Mary Ellen Zurko, Douglas W. Bonin, Andrew H. Mason, and Clifford E. Kahn. "A Retrospective on the VAX VMM Security Kernel." IEEE Transactions on Software Engineering. 17(11):1147-1165 (November 1991).

Lecture

Fill me in.

6 Nov 2000

Multics

Readings

Jerome E. Saltzer. "Protection and th Control of Information Sharing in Multics." Communications of the ACM 17(7):388-402 (July 1974).

Michael D. Schroeder. "Engineering a Security Kernel for Multics." ACM Operating Systems Review. 9(5):25-32

Lecture

Fill me in.

13 Nov 2000

CAP and CAL/TSS

Readings

A. J. Herbert. "A New Protection Architecture for the Cambridge Capability Computer." Operating Systems Review 12(1):24-28

Douglas Cook. "The Cost of Using the CAP COmputer's Protection Facilities." Operating Systems Review 12(2):26-30

Butler W. Lampson and Howard E. Sturgis. "Reflections on an Operating System Design." Communications of the ACM 19(5):251-265 (May 1976)

Lecture

Fill me in.

20 Nov 2000

The Intel i432

Readings

Edward F. Gehringer and Robert P. Colwell "Fast Object-Oriented Procedure Calls: Lessons from the Intel 432." 1986 International Symposium on Computer Architecture, Tokyo, Japan. June 2-5, 1986, pp. 92-101.

Robert P. Colwell, Edward F. Gehringer, and E. Douglas Jensen. "Performance Effects of Architectural Complexity in the Intel 432." ACM Transactions on Computer Systems, 6(3):296-339 (August, 1988)

D. D. Redell and R. S. Fabry. "Selective Revocation of Capabilities." Proc. INRIA Workshop on Operating Systems, 1974.

Lecture

Fill me in.

27 Nov 2000

L3/L4 and EROS

Readings

Jochen Liedtke. "A Persistent System in Real Use: Experiences of the First 13 Years." 1993 International Workshop on Object-Orientation in Operating Systems. Dec 5-8, 1993, Asheville, North Carolina.

Jochen Liedtke. "On Microkernel Construction." 15th ACM Symposium on Operating System Principles. Dec 3-6, 1995, Copper Mountain Resort, Colorado.

Jonathan S. Shapiro, Jonathan M. Smith, and David J. Farber. "EROS: A Fast Capability System.", Proc. 17th ACM Symposium on Operating System Principles. Published as Operating Systems Review 34(5):170-185 (Dec. 1999)

Jonathan S. Shapiro and Sam Weber. Verifying the EROS Confinement Mechanism. 2000 IEEE Symposium on Security and Privacy, Oakland, CA. pp. 166-176

Lecture

Fill me in.

4 Dec 2000

Assessments

Readings

Secure Computing Corporation. DTOS General System Security and Assurability Assessment Report Contract No. MDA904-93-C-4209, CDRL Sequence No. A011. Part Number 83-0902028A 001 Rev A, Version Date 28 June 1977.

Lecture

Fill me in.

11 Dec 2000

Review and Summary