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. |
Year | DOI | Venue |
---|---|---|
2004 | 10.1109/CSFW.2004.1310736 | CSFW |
Keywords | Field | DocType |
simple sequentialimperative language,typing rules permissive,array operation,information flow typing,array length,typing rule,lenient semantics,permissivetyping rule,program writing,sequential imperative language,typing rules,type system,programming language semantics,information flow security,out-of-bounds array index,array content,secure informationflow,out-of-bounds array indices,type theory,noninterference property,security class,τ1 arr τ2,lenient array operations,noninterference,practical secure information flow,security of data,indexing,computer science,computer security,java,information security,satisfiability | Information flow (information theory),Programming language,Of the form,Computer science,Information security,Type theory,Search engine indexing,Imperative programming,Theoretical computer science,Java,Semantics | Conference |
ISSN | ISBN | Citations |
1063-6900 | 0-7695-2169-X | 10 |
PageRank | References | Authors |
0.53 | 7 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Zhenyue Deng | 1 | 19 | 1.03 |
Geoffrey Smith | 2 | 10 | 0.53 |