Measuring information flow in software has recently become an active research topic in the security community. Information about confidential inputs may flow to public outputs in batch programs. It would be useful to quantify such flows in the computational world. In this paper, we present an automatic analyser for measuring information flow within software systems. We quantify leakage in terms of information theory and incorporate this computation into probabilistic semantics. Our semantic functions provide information flow measurement for programs given secure inputs under any probability distribution. The major contribution is an automatically quantitative analyser based on the leakage definition for such a language. While-loops are handled by applying entropy of generalized distributions and some properties e.g. the partition property and the mean entropy property in order to provide a more precise analysis with respect to the time of observation.

Boreale, M.. (2006). 'Quantifying information leakage in process calculi'. ICALP. Jul 9-16. Venice, Italy.

Clark, D., Hunt, S. and Malacaria, P. (2002). "Quantitative analysis of the leakage of confidential data", Electronic Notes in Theoretical Computer Science, 59 (3): 238-251.

Clark, D., Hunt, S. and Malacaria, P. (2005), "Quantitative information flow, relations and polymorphic types", J. Log. and Comput., 15(2):181-199.

Clark, D., Hunt, S. and Malacaria, P. (2007), "A static analysis for quantifying information flow in a simple imperative language", Journal of Computer Security, 15 (3):321-371.

Clarkson, M. R., Myers, A. C. and Schneider, F. B. (2005). 'Belief in information flow'. 18th IEEE Computer Security Foundations Workshop. Jun 20-22. Aix-en-Provence, France.

Clarkson, M. R., Myers, A. C. and Schneider, F. B. (2007), "Quantifying information flow with beliefs", Journal of Computer Security.

Denning,. D. E. R. (1976), "A lattice model of secure informatin flow", Communications of the ACM, 19 (5):236-243.

Denning,. D. E. R. (1982), Cryptography and Data Security, Addison-Wesley.

Di Pierro, A., Hankin C. and Wiklicky, H. (2002), 'Approximate non-interference'. CSFW. Jun 24-26. Cape Breton, Nova Scotia, Canada.

Di Pierro, A., Hankin C. and Wiklicky, H. (2004), "Approximate non-interference", Journal of Computer Security, 12(1):37-82.

Di Pierro, A., Hankin C. and Wiklicky, H. (2005), "Quantitative static analysis of distributed systems", J. Funct. Program., 15(5):703-749.

Goguen, J. A. and Meseguer, J. (1982). 'Security policies and security models'. IEEE Symposium on Security and privacy. April. Oakland, California, USA.

Gray III, J. W. (1991). 'Toward a mathematical foundation for informatin flow security'. IEEE Security and Privacy. April. Oakland, California, USA.

Kozen, D. (1981), "Semantics of probabilistic programs", Journal of Computer and System Sciences, 22(3):328-350.

Lowe, G. (2004), "Defining information flow quantity", Journal of Computer Security, 12(3-4):619-653.

Malacaria, P. (2007). 'Assessing security threats of looping constructs'. Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. Jan 17-19. Nice, France. ACM Press.

McIver, A. and Morgan, C. (2003). "A probabilistic approach to information hiding", Programming methodology: 441-460.

McIver, A. and Morgan, C. (2004), Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science), SpringerVerlag.

McLean, J. (1990). 'Security models and information flow'. Proceeding of the 1990 IEEE Symposium on Security and Privacy. May. Oakland, California, USA.

Millen, J. (1987). 'Covert channel capacity'. Proceeding 1987 IEEE Symposium on Resarch in Security and Privacy. Apr. Oakland, California, USA.

Monniaux, D. (2000). 'Abstract interpretation of probabilistic semantics'. SAS'00: Proceedings of the 7th International Symposium on Static Analysis. Jun 29 - Jul 1. London, UK.

Monniaux, D. (2001). 'Backwards abstract interpretation of probabilistic programs'. ESOP'01: Proceedings of the 10th European Symposium on Programming Languages and Systems. Apr 2-6. Genova, Italy.

Renyi, A. (1961). On measures of entropy and information. In Proceedings of the 4th Berkeley Symposium on Mathematics, Statistics and Probability, pages 547-561.

Renyi, A. (1970), Probability theory. North-Holland Publishing Company, Amsterdam.

Rokhlin, V. A. (1965), "Lectures on the entropy theory of measure-preserving transformations", Russian Mathematical Surveys, 22(5):1-52.

Rudin, W. (1966), Real and Complex Analysis, McGraw-Hill.

Weber, D. G. (1988). 'Quantitative hook-up security for covert channel analysis'. CSFW. Jun 9-11. Franconia, NH.

Wittbold, J. T. and Johnson, D. M. (1990). 'Information flow in nondeterministic systems'. IEEE Symposium on Security and Privacy. May. Oakland, California, USA.