Types and effects for non-interfering program monitors

Lujo Bauer; Jarred Ligatti; David Walker

doi:10.1007/3-540-36532-x_10

Types and effects for non-interfering program monitors

Lujo Bauer, Jarred Ligatti, David Walker

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter

6 Scopus citations

Abstract

A run-time monitor is a program that runs in parallel with an untrusted application and examines actions from the application's instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors. Our language provides a number of facilities for composing complex policies from simpler ones. We allow policies to be parameterized by values or other policies, and we define operators for forming the conjunction and disjunction of policies. Since the computations that implement these policies modify program behavior, naive composition of computations does not necessarily produce the conjunction (or disjunction) of the policies that the computations implement separately. We use a type and effect system to ensure that computations do not interfere with one another when they are composed.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Mitsuhiro Okada, Benjamin C. Pierce, Andre Scedrov, Hideyuki Tokuda, Akinori Yonezawa
Publisher	Springer Verlag
Pages	154-171
Number of pages	18
ISBN (Print)	3540007083
DOIs	https://doi.org/10.1007/3-540-36532-x_10
State	Published - 2003

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2609
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-36532-x_10

Cite this

Bauer, L., Ligatti, J., & Walker, D. (2003). Types and effects for non-interfering program monitors. In M. Okada, B. C. Pierce, A. Scedrov, H. Tokuda, & A. Yonezawa (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 154-171). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2609). Springer Verlag. https://doi.org/10.1007/3-540-36532-x_10

Bauer, Lujo ; Ligatti, Jarred ; Walker, David. / Types and effects for non-interfering program monitors. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Mitsuhiro Okada ; Benjamin C. Pierce ; Andre Scedrov ; Hideyuki Tokuda ; Akinori Yonezawa. Springer Verlag, 2003. pp. 154-171 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{ea3f7765f18e44d69011ab18d1655ee1,

title = "Types and effects for non-interfering program monitors",

abstract = "A run-time monitor is a program that runs in parallel with an untrusted application and examines actions from the application's instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors. Our language provides a number of facilities for composing complex policies from simpler ones. We allow policies to be parameterized by values or other policies, and we define operators for forming the conjunction and disjunction of policies. Since the computations that implement these policies modify program behavior, naive composition of computations does not necessarily produce the conjunction (or disjunction) of the policies that the computations implement separately. We use a type and effect system to ensure that computations do not interfere with one another when they are composed.",

author = "Lujo Bauer and Jarred Ligatti and David Walker",

year = "2003",

doi = "10.1007/3-540-36532-x_10",

language = "English (US)",

isbn = "3540007083",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "154--171",

editor = "Mitsuhiro Okada and Pierce, {Benjamin C.} and Andre Scedrov and Hideyuki Tokuda and Akinori Yonezawa",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "Germany",

}

Bauer, L, Ligatti, J & Walker, D 2003, Types and effects for non-interfering program monitors. in M Okada, BC Pierce, A Scedrov, H Tokuda & A Yonezawa (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2609, Springer Verlag, pp. 154-171. https://doi.org/10.1007/3-540-36532-x_10

Types and effects for non-interfering program monitors. / Bauer, Lujo; Ligatti, Jarred; Walker, David.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Mitsuhiro Okada; Benjamin C. Pierce; Andre Scedrov; Hideyuki Tokuda; Akinori Yonezawa. Springer Verlag, 2003. p. 154-171 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2609).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

TY - CHAP

T1 - Types and effects for non-interfering program monitors

AU - Bauer, Lujo

AU - Ligatti, Jarred

AU - Walker, David

PY - 2003

Y1 - 2003

N2 - A run-time monitor is a program that runs in parallel with an untrusted application and examines actions from the application's instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors. Our language provides a number of facilities for composing complex policies from simpler ones. We allow policies to be parameterized by values or other policies, and we define operators for forming the conjunction and disjunction of policies. Since the computations that implement these policies modify program behavior, naive composition of computations does not necessarily produce the conjunction (or disjunction) of the policies that the computations implement separately. We use a type and effect system to ensure that computations do not interfere with one another when they are composed.

AB - A run-time monitor is a program that runs in parallel with an untrusted application and examines actions from the application's instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors. Our language provides a number of facilities for composing complex policies from simpler ones. We allow policies to be parameterized by values or other policies, and we define operators for forming the conjunction and disjunction of policies. Since the computations that implement these policies modify program behavior, naive composition of computations does not necessarily produce the conjunction (or disjunction) of the policies that the computations implement separately. We use a type and effect system to ensure that computations do not interfere with one another when they are composed.

UR - http://www.scopus.com/inward/record.url?scp=35248842056&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248842056&partnerID=8YFLogxK

U2 - 10.1007/3-540-36532-x_10

DO - 10.1007/3-540-36532-x_10

M3 - Chapter

AN - SCOPUS:35248842056

SN - 3540007083

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 154

EP - 171

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Okada, Mitsuhiro

A2 - Pierce, Benjamin C.

A2 - Scedrov, Andre

A2 - Tokuda, Hideyuki

A2 - Yonezawa, Akinori

PB - Springer Verlag

ER -

Bauer L, Ligatti J, Walker D. Types and effects for non-interfering program monitors. In Okada M, Pierce BC, Scedrov A, Tokuda H, Yonezawa A, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2003. p. 154-171. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-36532-x_10

Types and effects for non-interfering program monitors

Abstract

Publication series

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this