• William Guenther, Mass Insight Global Partnerships and
  Robert Brammer, Brammer Technology, LLC.
  Slides
  Abstract:

  The Advanced Cyber Security Center research strategy focuses on leveraging the breadth and depth of the region's activities in the wide range of disciplines comprising cyber security. New England is unique in having a combination of leading corporations and universities in technology, business management, finance, law, economics, psychology, medicine and other areas critical to defending against the cyber security threat.

  In this presentation, we will discuss:

  1. The Advanced Cyber Security Center and its evolving R+D and education collaborations between industry, universities and government, and
  2. A few examples of ACSC research projects that focus on interdisciplinary approaches to large cyber security problems. The first example involves the integration of cyber security risk into an overall enterprise risk framework. The second involves techniques to analyze very large and volatile data sets while meeting constraints imposed by privacy and security regulations.

• Information-Flow Security for a Core of JavaScript
      Daniel Hedin, Andrei Sabelfeld
• Secure Information Flow for Concurrent Programs under Total Store Order
      Jeffrey A. Vaughan, Todd Millstein
• ENCOVER: Symbolic Exploration for Information Flow Security
      Musard Balliu, Mads Dam, Gurvan Le Guernic
• Information-flow control for programming on encrypted data
      John C. Mitchell, Rahul Sharma, Deian Stefan, Joe Zimmerman

• Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings
      Alisa Pankova, Peeter Laud
• Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
      Benedikt Schmidt, Simon Meier, Cas Cremers, David Basin
• Verifying privacy-type properties in a modular way
      Myrto Arapinis, Vincent Cheval, Stéphanie Delaune

• Security Analysis of Access Control through Program Verification
      Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato
• Gran: model checking grsecurity RBAC policies
      Michele Bugliesi, Stefano Calzavara, Riccardo Focardi, Marco Squarcina
• Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction
      Valerio Genovese, Deepak Garg, Daniele Rispoli

• Securing Interactive Programs
      Willard Rafnsson, Daniel Hedin, Andrei Sabelfeld
• Learning is Change in Knowledge: Knowledge-based Security for Dynamic Policies
      Aslan Askarov, Stephen Chong

• Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication
      Zhengqin Luo, Tamara Rezk
• Secure compilation to modern processors
      Pieter Agten, Raoul Strackx, Bart Jacobs, Frank Piessens
• Cache-leakage resilient OS isolation in an idealized model of virtualization
      Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna
• A Framework for the Cryptographic Verification of Java-like Programs
      Ralf Kuesters, Tomasz Truderung, Juergen Graf

• Constructing Optimistic Multi-party Contract Signing Protocols
      Barbara Kordy, Sasa Radomirovic
• Refining Key Establishment
      Christoph Sprenger, David Basin
• Discovering Concrete Attacks on Website Authorization by Formal Analysis
      Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis

• Measuring Information Leakage using Generalized Gain Functions
      Mário S. Alvim, Kostas Chatzikokolakis, Catuscia Palamidessi, Geoffrey Smith
• The Thermodynamics of Confidentiality
      Pasquale Malacaria, Fabrizio Smeraldi

• GlassTube: A Lightweight Approach to Web Application Integrity [abstract], Andrei Sabelfeld
• Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems [abstract], Alejandro Russo
• Enforcing Information Flow Policies by a Three-valued Analysis [abstract], Nadia Tawbi
• Precise Enforcement of Progress-Sensitive Security [abstract], Scott Moore
• Formalizing and Enforcing Purpose Restrictions on Information Use [abstract], Michael Tschantz
• Revoke and Let Live—A Secure Key Revocation API for Cryptographic Devices [abstract], Cyrille Wiedling
• The "Million Message Attack" in 15,000 Messages [abstract], Graham Steel
• A Session Mix-up Attack on the UMTS/LTE Authentication and Key Agreement Protocols [abstract], Stig Mjølsnes
• Clash Attacks on the Verifiability of E-Voting Systems [abstract], Ralf Küsters
• Type-based analysis of real PKCS#11 devices [abstract], Riccardo Focardi
• Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions [abstract], Catherine Meadows
• Formalizing Physical Security Procedures [abstract], Catherine Meadows
• Proving Computational Security with a General-Purpose C Verifier [abstract], François Dupressoir
• Synthesis of Public-Key Encryption Schemes [abstract], Gilles Barthe
• Differential Privacy with Arbitrary Metrics [abstract], Kostas Chatzikokolakis
• Privacy in Geolocation Systems [abstract], Miguel Andres

• Butler Lampson, Microsoft Research
  Talk title: Retroactive Security.
  Abstract:

  It's time to change the way we think about computer security: instead of trying to prevent security breaches, we should focus on dealing with them after they happen. Today computer security depends on access control, and it's been a failure. Real world security, by contrast, is mainly retroactive: the reason burglars don't break into my house is that they are afraid of going to jail, and the financial system is secure mainly because almost any transaction can be undone.

  There are many ways to make security retroactive:

  • Track down and punish offenders.
  • Selectively undo data corruption caused by malware.
  • Require applications and online services to respect people's ownership of their personal data.

  Access control is still needed, but it can be much more coarse-grained, and therefore both more reliable and less intrusive. Authentication and auditing are the most important features. Retroactive security will not be perfect, but perfect security is not to be had, and it will be much better than what we have now.

• Generic Indifferentiability Proofs of Hash Designs
      Marion Daubignard, Pierre-Alain Fouque, Yassine Lakhnech
• Automatically Verified Mechanized Proof of One-Encryption Key Exchange
      Bruno Blanchet
• Verified Security of Merkle-Damgaard
      Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin
• Provably Secure and Practical Onion Routing
      Michael Backes, Ian Goldberg, Aniket Kate, Esfandiar Mohammadi

CSF attendees are welcome to attend the lecture. Public transit tickets will be provided to allow attendees to travel to and from DSN. Google map directions are here. A handy PDF handout is here.

• Eighth Workshop on Formal and Computational Cryptography (FCC)
  Location: Pierce Hall, Room 209

• Eighth Workshop on Formal and Computational Cryptography (FCC)
  Location: Maxwell-Dworkin Hall, Room 119
• 6th International Workshop on Analysis of Security APIs (ASA)
  Location: Pierce Hall, Room 209

• 6th International Workshop on Analysis of Security APIs (ASA)
  Location: Pierce Hall, Room 209

• 2nd Workshop on Socio-Technical Aspects in Security and Trust (STAST)
  Location: Maxwell-Dworkin Hall, Room G 135