Array operations for secure information flow

Array operations exist in many nontrivial programs. Array operations can cause subtle information leaks. Many type systems of secure information flow have been developed, however, so far little type system attention to secure information flow of discretional array operations. This paper allows array as first-class value and encodes multidimensional array as array of array by alias array. The soundness of our type system is proved by noninterference.