Logic and Verification Methods in Security and Privacy
NII Shonan Meeting:
@ Shonan Village Center, October 26-29, 2015
- Marco Gaboardi, University of Dundee, UK
- Vivek Nigam, Federal University of Paraiba, Brazil
- Tachio Terauchi, JAIST, Japan
Description of the meeting
Logic and verification methods are standard tools useful for reasoning in a formal way about programs. Tools and techniques based on logic have been used to prove software correct with respect to different requirements: functional correctness, resource consumption, integrity of data, etc. An area where the usefulness of these methods was observed early on is the one of security and privacy. Formal logic methods have been used for formally specifying security and privacy policies and models, and for verifying that programs respect them.
Recently however traditional notions of security and privacy have been extended to take into account new refined aspects of programs. In particular, we assisted at the extension of traditional security properties to notions that are quantitative or probabilistic in nature, and to notions that require complex policies models based on different notions of capabilities or authorizations. Quantitative information flows, differential privacy and distance-bounding protocols are three important examples of such security properties. Quantitative information flows is a natural quantitative extension of the traditional information flow theory where the information that is leaked by a program is measured in terms of notions like min-entropy and gleakage. Differential privacy is a strong statistical notion of data privacy requiring that the result of a data analysis is probabilistically almost the same in the case the individual participate in the data or not. Distance-bounding protocols are cryptographic protocols where it is critical to control also the physical distance between the parties involved. These three properties are emblematic examples of the kind of security and privacy requirements that software is required today to ensure.
Verifying and reasoning in a formal way about this kind of security and privacy properties require extensions of traditional techniques that are able at the same time of describing more refined formal models – accounting for the quantities and/or capabilities specific to these properties – and more refined proof techniques designed specifically for these formal models. In order to deal with this supplementary complexity of the security and privacy models, several techniques have enriched traditional logical methods with quantitative informations – like probabilities, timestamps, etc – or authentication mechanisms – like capabilities, labels, etc. These techniques have provided new theoretical foundations and practical successful tools.
Part of this success is certainly to ascribe to the advancements in the technology of SMT solvers and interactive proof assistants. These advancements have permitted to reach
results that only few years ago seemed impossible to reach. SMT solvers and proof assistants can be nowadays easily integrated in tools for security and privacy analysis, and serve as basic component for the resolution of numeric and/or symbolic constraints relative to quantities and/or capabilities. However, the development of more and more specialized techniques require also a more and more customized use of these tools. For this reason it is important to promote the interaction between the members of the security and privacy community and the community working on verification tools.
The overall goal of the meeting is to foster the discussion between researchers in academia and industry that are working in different areas of security and privacy, logic and verification. The common ground between the different participants will be the use of logic and verification methods for formally reasoning about the different aspects of security and privacy. On the application side, we aim at fostering the discussion around the different tools that are needed to reason about traditional and quantitative notion of security and privacy. On the theoretical side instead, we aim at fostering the discussion around common foundations for the different aspects of security and privacy. A further goal of the meeting is exploring the applicability of the most recent techniques developed in the setting of security and privacy to problem in different research areas.
We plan to involve participants from different research areas of security and privacy as:
– Quantitative information flow
– Differential Privacy
– Distance-bounding protocols
– Information flow controls
– Access control policies – Anonymization
– Capabilities models
– Malware detection
Moreover, we plan to involve participants with specific expertise in logic and verification methods as:
– Relational Logics
– Linear type systems
– Coalgebraic methods
– Higher order verification methods
– Dependent type systems
– Abstract Interpretation
– Proof assistants
– SMT solvers
The meeting will encourage exchanges between researchers representing the different research areas and communities. The expected outcome of the meeting are new collaborations between participants traditionally working in separate research areas.