Control and synthesis of non-interferent timed systems

References

• Alur, R., & Dill, D. (1994). A theory of timed automata. Theoretical Computer Science, 126, 183–235.
   Web of Science ®Google Scholar
• Barbuti, R., & Tesei, L. (2003). A decidable notion of timed non-interference. Fundamenta Informaticae, 54, 137–150.
   Web of Science ®Google Scholar
• Barthe, G., Pichardie, D., & Rezk, T. (2007). A certified lightweight non-interference java bytecode verifier. In R. De Nicola (Ed.), Proceedings of the 16th European conference on Programming (ESOP'07) (pp. 125–140). Braga: Springer-Verlag.
   Google Scholar
• Benattar, G., Cassez, F., Lime, D., & Roux, O.H. (2009, September). Synthesis of non-interferent timed systems. In J. Ouaknine & F.W. Vaandrager (Eds.), Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'09), Lecture Notes in Computer Science (Vol. 5813, pp. 28–42). Budapest: Springer.
   Google Scholar
• Bortz, A., & Boneh, D. (2007). Exposing private information by timing web applications. In P. Patel-Schneider & P. Shenoy (Eds.), Proceedings of the 16th International Conference on World Wide Web (WWW ’07) (pp. 621–628). Banff, Alberta, Canada: ACM.
   Google Scholar
• Bossi, A., Piazza, C., & Rossi, S. (2007). Compositional information flow security for concurrent programs. Journal of Computer Security, 15, 373–416.
   Google Scholar
• Bouyer, P., D’Souza, D., Madhusudan, P., & Petit, A. (2003, July). Timed control with partial observability. In W.H. Jr & F. Somenzi (Eds.), Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), Lecture Notes in Computer Science (Vol. 2725, pp. 180–192). Boulder, CO: Springer.
   Google Scholar
• Cassez, F. (2009, June). The dark side of timed opacity. In J. H. Park, H.-H. Chen, M. Atiquzzaman, C. Lee, T, Kim, & S.-S. Yeo (Eds.), Proceedings of the 3rd International Conference on Information Security and Assurance (ISA'09), Lecture Notes in Computer Science (Vol. 5576, pp. 21–30). Seoul: Springer.
   Google Scholar
• Cassez, F., Dubreil, J., & Marchand, H. (2009, October). Dynamic observers for the synthesis of opaque systems. In Z. Liu & A.P. Ravn (Eds.), 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), Lecture Notes in Computer Science (Vol. 5799, pp. 352–367). Macao, China: Springer.
   Google Scholar
• Cassez, F., Dubreil, J., & Marchand, H. (2012). Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design, 40, 88–115.
   Web of Science ®Google Scholar
• Cassez, F., Mullins, J., & Roux, O.H. (2007). Synthesis of non-interferent systems. In V. Gorodetsky, I. Kotenko, & V. Skormin (Eds.), 4th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS'07), Communications in Computer and Information Science (Vol. 1, pp. 307–321). St. Petersburg, Russia: Springer.
   Google Scholar
• Čerāns, K. (1992). Decidability of bisimulation equivalence for parallel timer processes. In G. von Bochmann & D.K. Probst (Eds.), Proceedings of the Fourth Workshop on Computer-Aided Verification (CAV'92), Lecture Notes in Computer Science (pp. 302–315). Montreal, Canada: Springer-Verlag.
   Google Scholar
• D'Souza, D., & Madhusudan, P. (2002). Timed control synthesis for external specifications. In H. Alt & A. Ferreira (Eds.), 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS'02), Lecture Notes in Computer Science (Vol. 2285, pp. 571–582). Antibes-Juan les Pins, France: Springer.
   Google Scholar
• D'Souza, D., Raghavendra, K.R., & Sprick, B. (2005). An automata based approach for verifying information flow properties. Electronic Notes in Theoretical Computer Science, 135, 39–58.
   Google Scholar
• Felten, E.W., & Schneider, M.A. (2000). Timing attacks on Web privacy. In P. Samarati (Ed.), CCS ’00: Proceedings of the 7th ACM Conference on Computer and Communications Security, Athens (pp. 25–32). New York, NY: ACM Press.
   Google Scholar
• Finkel, O. (2005). On decision problems for timed automata. Bulletin of the European Association for Theoretical Computer Science, 87, 185–190.
   Google Scholar
• Focardi, R., Ghelli, A., & Gorrieri, R. (1997, September). Using non-interference for the analysis of security protocols. In H. Orman & C. Meadows (Eds.), Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols. Piscataway, NJ: Rutgers University.
   Google Scholar
• Focardi, R., & Gorrieri, R. (1997). The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 23, 550–571.
   Web of Science ®Google Scholar
• Focardi, R., & Gorrieri, R. (2001). Classification of security properties (Part I: Information flow). In R. Focardi & R. Gorrieri (Eds.), Foundations of Security Analysis and Design I: FOSAD 2000 Tutorial Lectures, Lecture Notes in Computer Science (Vol. 2171, pp. 331–396). Heidelberg: Springer-Verlag.
   Google Scholar
• Gardey, G., Mullins, J., & Roux, O.H. (2005, August). Non-interference control synthesis for security timed automata. In M. Backes & A. Scedrov (Eds.), 3rd International Workshop on Security Issues in Concurrency (SecCo'05), Electronic Notes in Theoretical Computer Science (pp. 33–53). San Francisco, CA: Elsevier.
   Google Scholar
• Hadj-Alouane, N.B., Lafrance, S., Lin, F., Mullins, J., & Yeddes, M. (2005a). Characterizing intransitive noninterference for 3-domain security policies with observability. IEEE Transaction on Automatic Control, 50, 948–958.
   Web of Science ®Google Scholar
• Hadj-Alouane, N.B., Lafrance, S., Lin, F., Mullins, J., & Yeddes, M. (2005b). On the verification of intransitive noninterference in multilevel security. IEEE Transactions on Systems, Man and Cybernetics, 35, 948–958.
   Web of Science ®Google Scholar
• Henzinger, T., & Kopke, P. (1997). Discrete-time control for rectangular hybrid automata. In P. Degano, R. Gorrieri, & A. Marchetti-Spaccamela (Eds.), International Colloquium on Automata, Languages and Programming (ICALP'97) (pp. 582–593). Bologna, Italy: Santa Barabara.
   Google Scholar
• Kammuller, F. (2008). Formalizing non-interference for a simple bytecode language in Coq. Formal Aspects of Computing, 20, 259–275.
   Web of Science ®Google Scholar
• Kocher, P.C. (1996). Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In N. Koblitz (Ed.), International Cryptology Conference (CRYPTO'96) (pp. 104–113). Santa Barabara, CA: Springer-Verlag.
   Google Scholar
• Kotcher, R., Pei, Y., Jumde, P., & Jackson, C. (2013). Cross-origin pixel stealing: timing attacks using CSS filters. In V. Gligor & M. Yung (Eds.), Proceedings of the 2013 ACM SIGSAC conference on computer and communications security (pp. 1055–1062). Berlin: ACM.
   Google Scholar
• Krohn, M., & Tromer, E. (2009). Noninterference for a practical DIFC-based operating system. In A. Myers & D. Evans (Eds.), Proceedings of the 2009 30th IEEE Symposium on Security and Privacy (pp. 61–76). Washington, DC: IEEE Computer Society.
   Google Scholar
• Kupferman, O., & Vardi, M. (1997). Synthesis with incomplete information. In H. Barringer, M. Fisher, D. Gabbay & G. Gough (Eds.), Proceedings of the 2nd International Conference on Temporal Logic (ICTL'97) (pp. 91–106). Manchester, UK: Kluwer.
   Google Scholar
• Lamouchi, H., & Thistle, J. (2000). Effective control synthesis for DES under partial observations. In IEEE Conference on Decision and Control (pp. 22–28). Sydney, Australia: IEEE.
   Google Scholar
• Laroussinie, F., & Schnoebelen, P. (2000). The state-explosion problem from trace to bisimulation equivalence. In J. Tiuryn (Ed.), Foundations of Software Science and Computation Structures (FoSSaCS 2000), Lecture Notes in Computer Science (Vol. 1784, pp. 192–207). Berlin, Germany: Springer-Verlag.
   Google Scholar
• Lin, F., & Wonham, W. (1988). On observability of discrete-event systems. Information Sciences, 44, 173–198.
   Web of Science ®Google Scholar
• Lin, F., & Wonham, W. (1995). Supervisory control of timed discrete-event systems under partial observation. IEEE Transactions on Automatic Control, 40, 558–562.
   Web of Science ®Google Scholar
• Maler, O., Pnueli, A., & Sifakis, J. (1995). On the synthesis of discrete controllers for timed systems. In E.W. Mayr, & C. Puech (Eds.), Annual Symposium on Theoretical Aspects of Computer Science (STACS ’95) (pp. 229–242). Munich, Germany: Springer.
   Google Scholar
• Mazaré, L. (2004). Using unification for opacity properties. In Workshop on Issues in the Theory of Security (WITS'04) (pp. 165–176). Barcelona, Spain.
   Google Scholar
• Moez, Y., Lin, F., & Ben Hadj-Alouane, N. (2009). Modifying security policies for the satisfaction of intransitive non-interference. IEEE Transactions on Automatic Control, 54, 1961–1966.
   Web of Science ®Google Scholar
• R. Focardi, R.G., & Martinelli, F. (2003). Real-time information flow analysis. IEEE Journal on Selected Areas in Communications, 21, 20–35.
   Web of Science ®Google Scholar
• Rushby, J. (1992). Noninterference, transitivity and channel-control security policies ( Technical Report CSL-92-02). Menlo Park, CA: SRI International.
   Google Scholar
• Sabelfeld, A., & Myers, A. (2003). Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21, 1–15.
   Web of Science ®Google Scholar
• Saboori, A., & Hadjicostis, C. (2008). Opacity-enforcing supervisory strategies for secure discrete event systems. In the 47th IEEE Conference on Decision and Control (pp. 889–894). Cancun, Mexico: IEEE.
   Google Scholar
• Stockmeyer, L.J., & Meyer, A.R. (1973). Word problems requiring exponential time: Preliminary report. In A.V. Aho, A.B. Borodin, R.L Constable, R.W. Floyd, M.A. Harrison, R.M. Karp, & H.R. Strong (Eds.), ACM Symposium on Theory of Computing (STOC'73) (pp. 1–9). San Diego, CA: ACM.
   Google Scholar
• Tasiran, S., Alur, R., Kurshan, R.P., & Brayton, R.K. (1996). Verifying abstractions of timed systems. In U. Montanari & V. Sassone (Eds.), Conference on Concurrency Theory (CONCUR'96), Lecture Notes in Computer Science (Vol. 1119, pp. 546–562). Pisa, Italy: Springer.
   Google Scholar
• van der Meyden, R., & Zhang, C. (2006). Algorithmic verification of noninterference properties. In M. Beek & F. Gadducci (Eds.), Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006), Electronic Notes in Theoretical Computer Science (Vol. 168, pp. 61–75). Amsterdam, The Netherlands: Elsevier.
   Google Scholar