Discretional Array Operations for Secure Information Flow

Abstract

Arrays exist in many nontrivial programs. Array operations can cause subtle information leaks. This paper allows array as first-class value and regards discretional array as array of array by alias array. 2τ is the Arrays are given types of the form security class of the array's alias. To distinguish array from its alias, we propose a novel binary memory model [