Logic and Verification Methods in Security and Privacy

Icon

NII Shonan Meeting Seminar 069

Meeting Date

Shonan Village Center, October 26-29, 2015

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

Overview

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.

Program

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

General Schedule

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

Participants

  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

Transportation

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) :

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.

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:

Organizers

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