T. Case, We consider the possible values of ? . ? If ? = H, then from Corollary 1, µ ? ? µ and ? ? ? ? . So µ ? ? ? . ? If ? = L, then ?, ?() ? e 1 : L and ?, ?(

. By-simple and . Security, there exist i, j s.t. µ(e 1 )=?(e 1 )=i and µ(e 2 )=?(e 2 )=j. Since µ? ? ?, there exists k ? 0 s.t µ(T )=n 0, k?1 , ?(T )=n 0 , . . . n k?1

@. If and ?. , By the SOS rule (UPDATE-ARR), µ = µ[T [i] := j] and ? = ?[T [i] := j]. So µ ? ? ? . ? else, from the SOS rule (UPDATE-ARR), µ = µ and ? = ?

T. Case-allocate, We consider two cases. ? if ? = H, then by Corollary 1, µ ? ? µ and ? ? ? ? . So µ ? ? ? . ? if ? = L, from the rule (ALLOCATE), ?, ?() e : L and from Simple Security µ(e)=?(e). So

C. Skip, From the SOS rule (NO-OP), µ = µ and ? = ?

R. 1. Amtoft, J. Hatcliff, and E. Rodríguez, Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays, Programming Languages and Systems, 19th European Symposium on Programming, pp.43-63, 2010.
DOI : 10.1007/978-3-642-11957-6_4

A. Annichini, A. Bouajjani, and M. Sighireanu, TReX: A Tool for Reachability Analysis of Complex Systems, Proceedings of the 13th International Conference on Computer Aided Verification, CAV '01, pp.368-372, 2001.
DOI : 10.1007/3-540-44585-4_34

URL : https://hal.archives-ouvertes.fr/hal-00110460

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, FAST: Fast Acceleration of Symbolic Transition Systems, Computer Aided Verification, 15th International Conference, CAV 2003, pp.118-121, 2003.
DOI : 10.1007/978-3-540-45069-6_12

URL : https://hal.archives-ouvertes.fr/hal-00084185

E. Bonelli, A. Compagnoni, and R. Medel, Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp.37-56, 2005.
DOI : 10.1109/CSFW.2001.930133

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.76.7690

Z. Deng and G. Smith, Lenient array operations for practical secure information flow, 17th IEEE Computer Security Foundations Workshop, p.115, 2004.

D. Denning, A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976.
DOI : 10.1145/360051.360056

D. Denning and P. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

S. Genaim and F. Spoto, Information Flow Analysis for Java Bytecode, Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005,Proceed- ings, pp.346-362, 2005.
DOI : 10.1007/978-3-540-30579-8_23

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.5499

N. Halbwachs and M. Péron, Discovering properties about arrays in simple programs, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp.339-348, 2008.
DOI : 10.1145/1379022.1375623

URL : https://hal.archives-ouvertes.fr/hal-00288274

T. Henzinger, T. Hottelier, and L. Kovács, Valigator: A Verification Tool with Bound and Invariant Generation, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, pp.333-342, 2008.
DOI : 10.1007/978-3-540-89439-1_24

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.1898

S. Hunt and D. Sands, On flow-sensitive security types, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.79-90, 2006.
DOI : 10.1145/1111037.1111045

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.4867

A. Myers, JFlow, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.228-241, 1999.
DOI : 10.1145/292540.292561

V. Perrelle and N. Halbwachs, An Analysis of Permutations in Arrays, Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, pp.279-294, 2010.
DOI : 10.1007/978-3-642-11319-2_21

URL : https://hal.archives-ouvertes.fr/hal-00456558

F. Pottier and V. Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems, vol.25, issue.1, pp.117-158, 2003.
DOI : 10.1145/596980.596983

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.6266

A. Sabelfeld and A. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, 2003.
DOI : 10.1109/JSAC.2002.806121

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.3979

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.167-188, 1996.
DOI : 10.3233/JCS-1996-42-304

URL : http://cisr.nps.edu/downloads/96paper_jcs.pdf

J. Yao and J. Li, Discretional array operations for secure information flow, Journal of Information and Computing Science, vol.1, issue.2, pp.67-77, 2007.