Abstract
A hyperproperty is a set of sets of finite or infinite traces over some fixed alphabet and can be seen as a very generic system specification. In this work, we define the notions of holistic and incremental hyperproperties. Systems specified holistically tend to be more intuitive but difficult to reason about, whereas incremental specifications have a straightforward verification approach. Since most interesting security-related hyperproperties are in the syntactic class of holistic hyperproperties, we introduce the process of incrementalization to convert holistic specifications into incremental ones. We then present three incrementalizable classes of holistic hyperproperties and a respective verification method.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aceto, L., Ingolfsdottir, A., Srba, J.: The Algorithmics of Bisimilarity. In: Advanced Topics in Bisimulation and Coinduction, pp. 100–172. Cambridge University Press (2011)
Agat, J.: Transforming out timing leaks. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000, pp. 40–53. ACM, New York (2000)
Alpern, B., Schneider, F.B.: Defining liveness. Technical report, Ithaca, NY, USA (1984)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW 2004: Proceedings of the 17th IEEE Workshop on Computer Security Foundations, p. 100. IEEE Computer Society, Washington, DC (2004)
Bohannon, A., Pierce, B.C., Sjöberg, V., Weirich, S., Zdancewic, S.: Reactive noninterference. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, CCS 2009, pp. 79–90. ACM, New York (2009)
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721–756. Elsevier (2007)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF 2008: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pp. 51–65. IEEE Computer Society, Washington, DC (2008)
Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18, 1157–1210 (2010)
Darvas, Á., Hähnle, R., Sands, D.: A Theorem Proving Approach to Analysis of Secure Information Flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005)
D’Souza, D., Holla, R., Raghavendra, K.R., Sprick, B.: Model-checking trace-based information flow properties. Journal of Computer Security 19, 101–138 (2011)
Focardi, R., Gorrieri, R.: A taxonomy of security properties for process algebras. Journal of Computer Security 3(1), 5–34 (1995)
Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, p. 75 (1984)
Hähnle, R., Pan, J., Rümmer, P., Walter, D.: Integration of a Security Type System into a Program Logic. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 116–131. Springer, Heidelberg (2007)
Huisman, M., Blondeel, H.-C.: Model-Checking Secure Information Flow for Multi-threaded Programs. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 148–165. Springer, Heidelberg (2012)
Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. Electronic Notes in Theoretical Computer Science, 19 (1999)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York (1992)
Mantel, H.: Unwinding Possibilistic Security Properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 238–254. Springer, Heidelberg (2000)
McLean, J.: A general theory of composition for a class of possibilistic properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996)
Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties: extended version. Technical Report CW 616, Katholieke Universiteit Leuven (December 2011)
Niqui, M., Rutten, J.: Coinductive predicates as final coalgebras. In: Matthes, R., Uustalu, T. (eds.) Proceedings of the 6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, September 12-13, pp. 79–85 (2009)
Pnueli, A.: The temporal semantics of concurrent programs. In: Proceedings of the International Sympoisum on Semantics of Concurrent Computation, pp. 1–20. Springer, London (1979)
Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy, SP 1995, pp. 114–127. IEEE Computer Society, Washington, DC (1995)
Rushby, J.: Noninterference, transitivity and channel-control security policies. Technical report (1992)
Rutten, J.J.M.M.: Automata and Coinduction (an Exercise in Coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194–218. Springer, Heidelberg (1998)
Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. Journal of Computer Security 9(1/2), 75–103 (2001)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Stirling, C.: Modal and temporal properties of processes. Springer-Verlag New York, Inc., New York (2001)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: IEEE Computer Security Foundations Workshop, p. 29 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milushev, D., Clarke, D. (2012). Towards Incrementalization of Holistic Hyperproperties. In: Degano, P., Guttman, J.D. (eds) Principles of Security and Trust. POST 2012. Lecture Notes in Computer Science, vol 7215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28641-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-28641-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28640-7
Online ISBN: 978-3-642-28641-4
eBook Packages: Computer ScienceComputer Science (R0)