Browse Prior Art Database

AN AXIOMATIC APPROACH TO INFORMATION FLOW IN PARALLEL PROGRAMS

IP.com Disclosure Number: IPCOM000148354D
Original Publication Date: 1899-Dec-30
Included in the Prior Art Database: 2007-Apr-12
Document File: 28 page(s) / 2M

Publishing Venue

Software Patent Institute

Related People

Andrews, Gregory R.: AUTHOR [+3]

Abstract

AN AXIOMATIC APPROACH TO AN AXIOMATIC APPROACH TO INFORMATION FLOW IN PARALLEL PROGRAMS Gregory R . Andrews Cornell University Richard P. Reitmah Syracuse University ABSTRACT This paper presents a new, axiomatic approach to information flow in seauential and parallel programs. Flow axioms that capture the informa- tion flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by a variety of exam- ples. The applications of flow proofs to cqrt/fy- ing information flow policies and solving the con- finement problem are considered. It is also shown that flow axioms and correctness axioms can be combined to form an even more powerful proof ays- tern, JCevworA ghrasep? information flow, informa- tion security, security ceptification, parallel programs, axiomatic logic, proof rules. Categories: 4.32, 4.35, 5.21, 5.24. This work was supported in part by NSF grant MCS 77-07554. Author's Addresses: Professor G . R . Andrews, Department of Computer Science, Cornell University, Ithaca, NY,14853.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 9% of the total text.

Page 1 of 28

AN AXIOMATIC APPROACH TO

[This page contains 1 picture or other non-text object]

Page 2 of 28

[This page contains 1 picture or other non-text object]

Page 3 of 28

      AN AXIOMATIC APPROACH TO INFORMATION FLOW IN PARALLEL PROGRAMS
Gregory R . Andrews

Cornell University

Richard P. Reitmah

Syracuse University

ABSTRACT

     This paper presents a new, axiomatic approach to information flow in seauential and parallel programs. Flow axioms that capture the informa- tion flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by a variety of exam- ples. The applications of flow proofs to cqrt/fy- ing information flow policies and solving the con- finement problem are considered. It is also shown that flow axioms and correctness axioms can be

combined to form an even more powerful proof ays- tern,
JCevworA ghrasep? information flow, informa- tion security, security ceptification, parallel programs, axiomatic logic, proof rules.

Categories: 4.32, 4.35, 5.21, 5.24.

This work was supported in part by NSF grant MCS 77-07554.
Author's Addresses: Professor G . R . Andrews, Department of Computer Science, Cornell University, Ithaca, NY,14853.

Professor R.P. Reitman, School of Computer and Information Sciences, 313 Link Hall, Syracuse University, Syracuse, NY, 13210.

[This page contains 1 picture or other non-text object]

Page 4 of 28

[This page contains 1 picture or other non-text object]

Page 5 of 28

- 2 -

hardware and software vrotectiea Bechan%ams are correct.

~ ~ d e P R o A C t r ~ ~ b i e
paper focusea on the problem of ascertelning t h e flows

~ W U m l m w ~ of intormation wlthln para11e1 pr08ra.s. The laterested reader ia referred t o I13.151 for discuaslons of r a l i d ~ t i ~ ~

Gregory R. Andrevs 8Cce.a ~ 0 1 i c 1 e s and to I14.171 for dlueusslons of validating protrot ion kornels.

, Cornell University
Ye vfew a syatea a s a large. parallel proprnm in u?:lch

Richard P. Reitman variables are the objects that contain information. state- ments define actions, and processes a r e the subjects that

take actions. Given a proEram that defines a specific rys- tem. an Intormatlon policy is validated by solving t h e


1. Int.roJu- bfUXS&n prohlem, namely by dettrmlning how informa- tion IIows between variables a s a result of profram execu-

cfinputer sYatrp is seoure i f the obfsots and inf0p.n-

tios.

tlon it contains can only be acceaaed i n ways authorized by
a Y Y A ~ e C u r i t t
p O l l ~ y has t o components: The informatlon flow problem has been examined previ- an aCCeS8 POHCY and an information pollcy. An access pelt- Q u ~ ~ Y
by several researcher* (see C31 for a survey). Soae

CY sPeeifie3 the actions that subjects, such a s users, can have advocated monitorlng program execution a t run-ti..

take m oblrets. surh aa f i l s . In informatlon pollay L6.7.141 while...