Title :
Lenient array operations for practical secure information flow
Author :
Deng, Zhenyue ; Smith, Geoffrey
Author_Institution :
Sch. of Comput. Sci., Florida Int. Univ., Miami, FL, USA
Abstract :
Our goal in this paper is to make secure information flow typing more practical. We propose simple and permissive typing rules for array operations in a simple sequential imperative language. Arrays are given types of the form τ1 arr τ2, where τ1 is the security class of the array´s contents and τ2 is the security class of the array´s length. To keep the typing rules permissive, we propose a novel, lenient semantics for out-of-bounds array indices. We show that our type system ensures a noninterference property, and we present an example that suggests that it will not be too difficult in practice to write programs that satisfy the typing rules.
Keywords :
programming language semantics; security of data; type theory; τ1 arr τ2; array content; array length; array operation; information flow security; information flow typing; lenient semantics; noninterference; out-of-bounds array indices; program writing; security class; sequential imperative language; typing rules; Computer science; Computer security; Conferences; Indexing; Information security; Java; Timing; Turning;
Conference_Titel :
Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE
Print_ISBN :
0-7695-2169-X
DOI :
10.1109/CSFW.2004.1310736