Access control based on execution history, Proceedings of NDSS'03, pp.107-121, 2003. ,
Transforming out timing leaks, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.40-53, 2000. ,
DOI : 10.1145/325694.325702
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9484
Verification of sequential and concurrent programs, 1991. ,
Mechanized Metatheory for the Masses: The PoplMark Challenge, Proceedings of TPHOLs'05, pp.50-65, 2005. ,
DOI : 10.1007/11541868_4
Locales and Locale Expressions in Isabelle/Isar, Proceedings of TYPES'03, pp.34-50, 2003. ,
DOI : 10.1007/978-3-540-24849-1_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.801
Stack-based access control and secure information flow, Journal of Functional Programming, vol.15, issue.2, pp.131-177, 2005. ,
DOI : 10.1017/S0956796804005453
Secure Information Flow and Pointer Confinement in a Java-like Language, Proceedings of CSFW'02, 2002. ,
Secure Information Flow by Self- Composition, Proceedings of CSFW'04, pp.100-114, 2004. ,
DOI : 10.1109/csfw.2004.1310735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.378.849
A Formal Executable Semantics of the JavaCard Platform, Proceedings of ESOP'01, pp.302-319, 2001. ,
DOI : 10.1007/3-540-45309-1_20
Formally verifying information flow type systems for concurrent and thread systems, Proceedings of the 2004 ACM workshop on Formal methods in security engineering , FMSE '04, pp.13-22, 2004. ,
DOI : 10.1145/1029133.1029136
URL : https://hal.archives-ouvertes.fr/inria-00000632
ULM: A Core Programming Model for Global Computing, Proceedings of ESOP'04, pp.234-248, 2004. ,
DOI : 10.1007/978-3-540-24725-8_17
Noninterference for Concurrent Programs, Proceedings of ICALP'01, pp.382-395, 2001. ,
DOI : 10.1007/3-540-48224-5_32
URL : https://hal.archives-ouvertes.fr/inria-00072334
Noninterference for concurrent programs and thread systems, Theoretical Computer Science, vol.281, issue.1-2, pp.109-130, 2002. ,
DOI : 10.1016/S0304-3975(02)00010-5
URL : https://hal.archives-ouvertes.fr/inria-00072334
Decidability and proof systems for language-based noninterference relations, Proceedings of POPL'06, pp.67-78, 2006. ,
Lenient array operations for practical secure information flow, Proceedings of CSFW'04, pp.115-124, 2004. ,
Classification of Security Properties, Foundations of Security Analysis and Design, pp.331-396, 2001. ,
DOI : 10.1007/3-540-45608-2_6
Bridging Language-Based and Process Calculi Security, Proceedings of FOS- SACS'05, pp.299-315, 2005. ,
DOI : 10.1007/978-3-540-31982-5_19
Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, pp.11-22, 1982. ,
DOI : 10.1109/SP.1982.10014
Information flow vs. resource access in the asynchronous pi-calculus, Proceedings of ICALP'00, pp.415-427, 2000. ,
DOI : 10.1145/570886.570890
Schedule-Carrying Code, Proceedings of EMSOFT'03, pp.241-256, 2003. ,
DOI : 10.1007/978-3-540-45212-6_16
Secure Information Flow as Typed Process Behaviour, Proceedings of ESOP'00, pp.180-199 ,
DOI : 10.1007/3-540-46425-5_12
A Uniform Type Structure for Secure Information Flow, Proceedings of POPL'02, pp.81-92, 2002. ,
A temporal logic characterisation of observational determinism, Proceedings of CSFW'06, pp.3-15, 2006. ,
A semantic approach to secure information flow, Science of Computer Programming, vol.37, issue.1-3, pp.1-3113, 2000. ,
DOI : 10.1016/S0167-6423(99)00024-6
A semantic approach to secure information flow, Proceedings of MPC'98, pp.254-271, 1998. ,
A unifying approach to the security of distributed and multi-threaded programs1, Journal of Computer Security, vol.11, issue.4, pp.615-676, 2003. ,
DOI : 10.3233/JCS-2003-11406
Combining Different Proof Techniques for Verifying Information Flow Security, Pre- Proceedings of LOPSTR'06, volume Raporta di Ricerca CS-2006-5, 2006. ,
DOI : 10.1007/978-3-540-71410-1_8
On declassification and the nondisclosure policy, Proceedings of CSFW'05, pp.226-240, 2005. ,
Typing noninterference for reactive programs, Proceedings of FCS'04, 2004. ,
DOI : 10.1016/j.jlap.2007.02.009
URL : https://hal.archives-ouvertes.fr/inria-00070413
Secure Object Sharing in Java Card, Proceedings of Usenix workshop on Smart Card Technology, 1999. ,
Machine-checked correctness of a secure information flow analyzer (preliminary report), 2003. ,
Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002. ,
DOI : 10.1007/3-540-45949-9
The Isabelle Reference Manual ,
A simple view of type-secure information flow in the pi-calculus, Proceedings of CSFW'02, pp.320-330, 2002. ,
A fully adequate shallow embedding of the ??-calculus in Isabelle/HOL with mechanized syntax analysis, Journal of Functional Programming, vol.13, issue.02, pp.415-451, 2003. ,
DOI : 10.1017/S0956796802004653
Noninterference, transitivity, and channel-control security policies, 1992. ,
Securing Interaction between Threads and the Scheduler, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006. ,
DOI : 10.1109/CSFW.2006.29
The Impact of Synchronisation on Secure Information Flow in Concurrent Programs, Proceedings of PSI'01, pp.227-241, 2001. ,
DOI : 10.1007/3-540-45575-2_22
Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003. ,
DOI : 10.1109/JSAC.2002.806121
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.3979
A Model for Delimited Information Release, Proceedings of ISSS'03, pp.174-191, 2004. ,
DOI : 10.1007/978-3-540-37621-7_9
A Per Model of Secure Information Flow in Sequential Programs, Proceedings of ESOP'99, pp.40-58, 1999. ,
DOI : 10.1007/3-540-49099-X_4
A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, pp.59-91, 2001. ,
Dimensions and principles of declassification, Proceedings of CSFW'05, 2005. ,
The ?-calculus: a Theory of Mobile Processes, 2001. ,
A new type system for secure information flow, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.115-125, 2001. ,
DOI : 10.1109/CSFW.2001.930141
Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.355-364, 1998. ,
DOI : 10.1145/268946.268975
URL : http://cisr.nps.edu/downloads/98paper_multithread.pdf
Formal analysis of an information flow type system for MicroJava (extended version), 2003. ,
A type-based approach to program security, Proceedings of TAPSOFT'97, pp.607-621, 1997. ,
DOI : 10.1007/BFb0030629
Probabilistic noninterference in a concurrent language, Proceedings. 11th IEEE Computer Security Foundations Workshop (Cat. No.98TB100238), pp.34-43, 1998. ,
DOI : 10.1109/CSFW.1998.683153
Probabilistic noninterference in a concurrent language, Proceedings. 11th IEEE Computer Security Foundations Workshop (Cat. No.98TB100238), pp.231-253, 1999. ,
DOI : 10.1109/CSFW.1998.683153
Verifying secrets and relative secrecy, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.268-276, 2000. ,
DOI : 10.1145/325694.325729
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.7333
Observational determinism for concurrent program security, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., pp.29-46, 2003. ,
DOI : 10.1109/CSFW.2003.1212703
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.3238