No.069 Logic and Verification Methods in Security and Privacy

Shonan Village Center, October 26-29, 2015

(Check-in: night before, Oct. 25, 2015)

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.

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.

	Monday	Tuesday	Wednesday	Thursday
9:00	Tutorial – Scedrov	Tutorial – Jacobs	Tutorial – Bana	Tutorial – Hsu
10:10	Break	Break	Break	Break
10:50	3 Research Problems Talcott, Kawamoto, Jia	3 Research Problems Ghilezan, Chong, Sands	3 Advertisements Okada, Baelde, Hirschi	1 Research Problems Giacobazzi
11:30			Tool overview – Stefan	Conclusion
12:00	Lunch	Lunch	Lunch	Lunch
13:30	Group Photo	Free time	Free time
14:00	Tutorial – Pavlovic	Tutorial – Gambs	Tutorial – Garg
15:00	2 Advertisements Nigam, Maffeis	2 Advertisements Hasuo, Izumi	2 Advertisements Dal Lago, Katsumata
15:30	Break	Break	Break
16:30	Talk -?Morgan	Talk – Hofmann	Tool demo – Russo
17:00	Open Panel Discussion	Open Panel Discussion	Open Panel Discussion
18:00	Dinner	Dinner	Dinner

Time allocated for the different kinds of talks:
Tutorial – 50 minutes
Research Problem talks – 15 minutes
Advertisement Talks – 10 minutes
Tool Overviews – 20 minutes
Others – 25 minutes

Day by Day Schedule

Monday October 26

9:00 – ?Tutorial
Andre Scedrov -?Multiset rewriting with dense time and the analysis of cyber-physical security protocols

10:10 – Break

10:50 – Research Problems
Carolyn Talcott -?Trust and Security Challenges for Networked Distributed Cyber-Physical Agent Systems
Yusuke Kawamoto?-?Combining Static and Statistical Approaches to Quantitative Information Flow
Limin Jia – Challenges in Engineering a Provably Secure Hypervisor Framework

12:00 – Lunch and Group Photo

14:00?- ?Tutorial
Dusko Pavlovic -?Cyber-physical security in actor networks

15:00 – Advertisement Talks
Vivek Nigam -?Timed Intruder Models
Sergio Maffeis – Automated Testing of Browser Security Policies

15:30 – Break

16:30 – Talk
Carroll Morgan?- Greatest pre-uncertainties for hyperGCL:
a backwards semantics for abstract HMM’s

17:00 – Open Panel Discussion

Tuesday October 27

9:00 – ?Tutorial
Bart Jacobs?-?Attribute-based authentication in practice

10:10 -?Break

10:50 -?Research Problems
Silvia Ghilezan -?Types in access control and privacy
Stephen Chong?-?Knowledge and Effect: A Logic for Reasoning about Confidentiality and Integrity Guarantees
Dave Sands -?Language-based Data Minimization.

12:00 -?Lunch

14:00?- ?Tutorial
Sébastien Gambs?-?Inference attacks in location data

15:00 -?Advertisement Talks
Ichiro Hasuo -?Kleisli Simulations, for Quantitative Verification (in General) and Probabilistic Anonymity (in Particular)
Takeuti Izumi?-?Logical system for negligible probability

15:30 -?Break

16:30 -?Talk
Martin Hofmann – GuideForce: type-based enforcement of secure coding guidelines

17:00 -?Open Panel Discussion

Wednesday?October 28

9:00 – ?Tutorial
Gergei Bana?-?Computationally Sound Security Analysis with First Order Logic – An Introduction to the Computationally Complete Symbolic Attacker Based on Indistinguishability

10:10 -?Break

10:50 – Advertisement Talks
Mitsuhiro Okada – French-Japanese cybersecurity framework (with special focus on formal methods)
David Baelde?-?Partial Order Reduction for Security Protocols: Improving Automated Trace Equivalence Checking in the Symbolic Model
Lucca Hirschi?-?Automatic Verification of Privacy Protection for Unbounded Sessions

11:30 – Tool Overview
Deian Stefan -?Building Least Privileged Web Applications with Node.js

12:00 -?Lunch

14:00?- ?Tutorial
Deepak Garg?-?CostIt: Using dependent types and co-monads for incremental complexity analysis

15:00 -?Advertisement Talks
Ugo Dal Lago?-?On Equivalences, Metrics, and Polynomial Time
Sin-ya Katsumata?-?TBA

15:30 -?Break

16:30 -?Tool Demo
Alejandro Russo?-?Two can keep a secret if one of them uses Haskell

17:00 -?Open Panel Discussion

Thursday October 29

9:00 – ?Tutorial
Justin Hsu?-?An introduction to language-based techniques for verifying differential privacy

10:10 -?Break

10:50 – Research Problems
Roberto Giacobazzi?- Towards systematic code obfuscation (theory and practice)

11:30 – Conclusion

12:00 -?Lunch

	Sunday	Monday	Tuesday	Wednesday	Thursday
7:30		Breakfast	Breakfast	Breakfast	Breakfast
9:00		Meeting	Meeting	Meeting	Meeting
10:10		Break	Break	Break	Break
10:50		Meeting	Meeting	Meeting	Meeting
12:00		Lunch	Lunch	Lunch	Lunch
13:30		Group Photo	Break	Break
14:00		Meeting	Meeting	Meeting
15:30	Check-in time	Break	Break	Break
16:30	Check-in time	Meeting	Meeting	Meeting
18:00	Check-in time	Dinner	Dinner	Main Banquet
19:00	Welcome dinner	Dinner	Dinner	Main Banquet
19:30	Welcome dinner	Free discussions time	Free discussions time	Main Banquet
20:00	Welcome dinner	Free discussions time	Free discussions time	Free discussions time

1. Aslan Askarov, Aarhus University
2. David Baelde, LSV, ENS Cachan
3. Gergei Bana, INRIA Paris-Rocquencourt
4. Stephen Chong Harvard University
5. Marco Gaboardi, University of Dundee
6. Sébastien Gambs, Université de Rennes 1 ? Inria
7. Deepak Garg, Max Planck Institute for Software Systems
8. Silvia Ghilezan, University of Novi Sad
9. Roberto Giacobazzi, University of Verona and IMDEA Software
10. Ichiro Hasuo, The University of Tokyo
11. Martin Hofmann, LMU Munich
12. Lucca Hirschi, LSV, ENS Cachan
13. Justin Hsu, University of Pennsylvania
14. Bart Jacobs, Radboud University Nijmegen
15. Limin Jia, Carnegie Mellon University
16. Shin-ya Katsumata, RIMS/ Kyoto University
17. Yusuke Kawamoto, INRIA & LIX Ecole Polytechnique
18. Ugo Dal Lago, University of Bologna & INRIA
19. Sergio Maffeis, Imperial College London
20. Carrol Morgan, UNSW, Australia
21. Vivek Nigam, Federal University of Paraiba
22. Mizuhito Ogawa, JAIST
23. Mitsuhiro Okada, Keio University
24. Dusko Pavlovic, University of Hawaii at Manoa
25. Alejandro Russo, Chalmers
26. David Sands, Chalmers University of Technology
27. Andre Scedrov, University of Pennsylvania
28. Deian Stefan, Stanford University
29. Kohei Suenaga, Kyoto U.
30. Izumi Takeuti, AIST
31. Carolyn Talcott, SRI International
32. Tachio Terauchi, Japan Advanced Institute of Science and Technology
33. Santiago Zanella-Beguelin, MSR ? INRIA

Please note that the entrance of Shonan Village Center is closed between 11:00pm ? 7:00am. Prior arrangement is required to enter the center after 11:00pm.

Access to Shonan Village:

See
Access to Shonan Village center
Shonan Village Home Page

There are several routes from Tokyo area or Narita airport. In general, first move by a train to? either Zushi (JR) or Shin-Zushi (Keikyu), and then take a bus or a taxi. For foreigners, we would recommend sharing a? taxi from Zushi or Shin-Zushi. The train route/schedule can be searched by using the train route finder below.

Train Schedule Search (not for reservation) :

• Jordan Train Route Finder?

For destination, enter “Zushi” or “Shin-Zushi”.? As Tokyo area is served by several companies, you will see several choices. Please pick one that seems most convenient. An optimal route depends on the departure time.

• Narita Airport Access Planner

You can search a train schedule from/to Narita Airport.

Recommended routes from Tokyo/Airports to Zushi:

Note: The following may not be the best route, depending on the time of departure.

• From Tokyo Narita Airport

Take JR Narita Express to go to “Ofuna” or “Yokohama”, and then take JR Yokosuka Line to Zushi.

• From Tokyo Haneda Airport

Take Keikyu Haneda Airport Line. Change at Keikyu Kamata station to Keikyu Line, and then change at Kanazawa-Hakkei to Keikyu Zushi Line and get off at Shin-Zushi terminal.

From Zushi or Shin-Zushi to Shonan Village Center

At Zushi station, go out from “East Exit”.

Please take a bus (which leaves once in an hour or half an hour, and takes 30 min from Zushi to Shonan Village Center) or a taxi, which costs approximately 3,000 yen and takes about 20 min.

Bus Time Table

Please take bus number 16 that leaves from Bus Stop #1 of the east exit of JR Zushi station, and costs 350 yen.

There are buses that leave from #1 and? go to other destination. So, make sure that the final destination of the bus is “Shonan Kokusai-mura Center” (the destination sign is in Japanese? but it comes with number “16”; if you are not sure, please ask the driver or other passengers before boarding), and get off at the final stop. Shonan Village Center is on the righthand side of the bus stop.

As a bus driver is not likely to speak English, we recommend sharing a taxi (or finding a company who speaks Japanese, to take a bus).

Here?are some Japanese messages to show to a taxi driver.

Other Links on Travel Information:

• Tokyo Narita Airport
• JR Central
• JR East

• Marco Gaboardi, University of Dundee, UK
• Vivek Nigam, Federal University of Paraiba, Brazil
• Tachio Terauchi, JAIST, Japan