Chalmers Security Seminar

Description

The Chalmers Security Seminar aims at boosting communication between different groups at Chalmers as well as the outside (academia and industry) communities about computer security. Our ambition is that every second week a speaker from academia or industry presents cutting-edge research to the security fellows at Chalmers. We very much welcome contributions by internal speakers (PhD students, PostDocs, Faculty) fulfilling, but not limited to, the following criteria:

It is a fundamental paper for some security area (a survey, ...)
It has received a best-paper award or similar in a top-tier venue
It is currently relevant for our own security research

Time: Fridays 11-12

Upcoming Activities

Activity: Talk
Time: Thursday October 19, 15:00
Location: Room 8103
Speaker: Somesh Jha, University of Wisconsin (Madison)
Title: Synthesis Techniques for Security
Abstract:
The problem of implementing a secure program is an ideal problem domain for formal methods. Even a small error in the logic of a program can drastically weaken the security guarantees that it provides. Existing work on applying formal methods to security has focused primarily on applying verification techniques to determine if an existing program satisfies a desired security guarantee. In this talk, I propose that many problems in secure programming can instead be addressed by synthesizing a provably-secure program automatically. We review some work on automatically instrumenting programs that satisfy security properties expressible as safety properties and on a general framework for designing program synthesizers. I will then describe a potential line of work on automatically synthesizing programs that simultaneously satisfy security and functionality.

Past Activities

Activity: Talk
Time: Thursday May 4, 15:00
Location: EDIT-Room, 3364
Speaker: Pablo Buiras, Harvard
Title: CLIO: Cryptographically Secure Information Flow Control on Key-Value Stores
Abstract:
Cryptography can in principle be used to protect users' data when stored or transmitted, but in practice is error-prone and can potentially result in a violation of a user's security concerns. Information flow control (IFC) systems, on the other hand, can automatically enforce security policies on data with policy languages expressive enough to capture many desired confidentiality and integrity requirements. In this talk I will present CLIO, an Information flow control (IFC) system that transparently incorporates cryptography to enforce confidentiality and integrity policies on untrusted key-value storage. CLIO insulates developers from explicitly manipulating keys and cryptographic primitives by leveraging the policy language of the IFC system to automatically use the appropriate keys and correct cryptographic operations. Our system relies on a CPA-secure cryptosystem, and we show that CLIO is secure with a novel proof technique composing cryptographic proof techniques with standard programming language techniques.

Activity: Talk
Time: Tuesday April 18, 10:00
Location: Room 4128
Speaker: Kim Kling, Adrian Bjugård
Title: Navigational Security Policy for the Web
Abstract:
There is currently no client-side enforceable way for administrators or developers to define the set of legal destinations from within a web application. This allows an attacker to cause navigation to unwanted destinations, if content from the attacker has been included. We present Navigational Security Policy, a method for web applications to provide the complete set of legal destinations, to be enforced by web clients. We show that it works in a proof of concept implementation by applying navigational policies on real world web applications.

Activity: Talk
Time: Thursday April 6, 9:30
Location: Room 8103
Speaker: Ben Stock, CISPA Saarbrucken
Title: Historical Analyses of the Client-Side Web Security and How to tell people they have an issue
Abstract:
In this talk, I will present two lines of research I am currently pursuing. On the one hand, my work focusses on client-side Web security. To better understand how the eco system evolved, we conducted a historical study of the last 20 years of the Web using data from the Internet Archive. Given that the Archive stores all client-side code as well as relevant header information, this enabled us to analyze trends over the last years, which allow us to draw conclusions on how future security mechanisms should be implemented.

On the other hand, while as a community we have become very good at discovering vulnerabilities at scale (regardless of Web or network level flaws), informing the affected parties about the issues has only been treated as a side note in previous research. To understand how such notifications can be conducted at scale, we conducted an experiment in which we notified more than 44,000 vulnerable domains, using different communication channels. Our work shows that reaching administrators is the biggest roadblock to a successful notification. In my talk, I will also discuss some of the technical and human challenges we face when notifying at scale, moreover highlighting which of these areas require further research.

Bio:
Ben Stock is a postdoctoral researcher at the Center for IT-Security, Privacy and Accountability (CISPA) in Saarbruecken. Apart from having a background in malware analysis, Ben focussed on Web security for his PhD thesis, covering different client-side security challenges. His research nowadays not only focusses on the detection and mitigation of Web vulnerabilities as well as the general area of network security, but more broadly also on how large-scale detection of vulnerabiltiies can be transformed into large-scale fixing of the discovered vulnerabilities. In his spare time, he also enjoys the challenges brought up in Capture the Flag competitions.

Activity: Talk
Time: Monday March 13, 15:00
Location: EDIT-Room, 3364
Speaker: Daniel Huang, Harvard University PhD student
Title: Compiling Probabilistic Programs
Abstract:
In this talk, we will present some of our recent work on probabilistic programming languages. In the first half of the talk, we will describe a semantics for these languages based on Type-2 computable distributions. Such an approach enables us to reason denotationally about probabilistic programs as well as in terms of sampling. In the second half, we will describe a compiler for a simple probabilistic programming language. The compiler uses a sequence of intermediate languages to gradually and successively transform a specification of a probabilistic model into a Markov Chain Monte Carlo inference algorithm for execution on the CPU or GPU.

https://danehuang.github.io/

Activity: Talk
Time: Thursday August 25, 14:00
Location: Room 8103
Speaker: Associate Professor Claudio Orlandi (Aarhus University)
Title: ZKBoo: Faster Zero-Knowledge for Boolean Circuits
Abstract:
In this talk we describe ZKBoo, a proposal for practically efficient zero-knowledge arguments especially tailored for Boolean circuits and report on a proof-of-concept implementation. As an highlight, we can generate (resp. verify) a non-interactive proof for the SHA-1 circuit in approximately 13ms (resp. 5ms), with a proof size of 444KB. Our techniques are based on the “MPC-in-the-head” approach to zero-knowledge of Ishai et al. (IKOS), which has been successfully used to achieve significant asymptotic improvements. Our contributions include: 1) A thorough analysis of the different variants of IKOS, which highlights their pro and cons for practically relevant soundness parameters; 2) A generalization and simplification of their approach, which leads to faster Sigma-protocols (that can be made non-interactive using the Fiat-Shamir heuristic) for statements of the form “I know x such that y = f(x)” (where f is a circuit and y a public value); 3) A case study, where we provide explicit protocols, implementations and benchmarking of zero-knowledge protocols for the SHA-1 and SHA-256 circuits;

The paper was published at USENIX Security Symposium 2016 and received best paper award.

Activity: Master's thesis defense
Time: Wednesday June 8, 10:00
Location: Room 8103
Speaker: Niklas Andreasson
Title: Enhancing the COWL W3C Standard
Abstract:
Web applications are often composed by resources such as JavaScript written, and provided, by different parties. This reuse leads to questions concerning security, and whether one can trust that third-party code will not leak users’ sensitive information. As it stands today, these concerns are well-founded.

With the web’s current security primitives there is a trade-off between developer flexibility and user privacy. If developers choose to include untrusted code then users’ privacy suffers. On the other hand, if developers abstain from reusing third-party code, user privacy is favoured, on the cost of developer flexibility. This trade-off can partly be attributed to the fact that the security primitives are discretionary, where untrusted code either is granted or denied access to data. After code has been granted access to data there is no further attempt to verify that the data is used properly.

In 2014, Stefan et al. proposed a security mechanism which called COWL (Confinement of Origin Web Labels). COWL is a mandatory access control which is able to let untrusted code compute on sensitive information, while confining it. Through this, COWL is able to address some of the shortcomings of the web’s current security mechanisms, and in the end effectively eliminate the trade-off that exists. Since the introduction of COWL, it has gone on to become a W3C standard.

This thesis evaluates the COWL W3C specification by deploying it in Mozilla Firefox. While COWL aims to mainly address information leaks caused by bugs, we bring the specification towards addressing malicious code by highlighting two covert channels: one due to the browser layout engine, and another due to browser optimizations. Furthermore, we implement two case studies which shows how COWL can be used, and as part of this, note some practical problems.Through the thesis we managed to make contributions to the COWL W3C specification.

Activity: Talk
Time: Wednesday June 8, 14:30
Location: Room 8103
Speaker: Peter Y A Ryan (University of Luxembourg)
Title: Selene: Voting with Transparent Verification and Coercion Mitigation
Abstract:
In conventional cryptographic E2E verification schemes, voters are provided with encrypted ballots that enable them to confirm that their vote is accurately included in the tally. Technically this is very appealing, but voters, election officials etc. need to understand some rather subtle arguments to appreciate the integrity and ballot secrecy guarantees provided by such mechanisms.

A simple way to achieve a degree of verifiability and ballot privacy is to provide each voter with a unique, private tracking number. Votes are posted on a bulletin board in the clear along with their tracking number. Thus voters can visit the WBB confirm that there is an entry with their tracking number showing the correct vote. The beauty of this approach is its simplicity and understandability. There are, however, two drawbacks: we must ensure that trackers are unique and a coercer can demand that the voter reveal her tracking number. It is interesting to note that the coercer must ask for the tracker before posting. If he asks after posting the voter has a simple strategy to fool him: just reads off a tracker number with the coercer's required vote from the WBB.

In this talk, I describe a scheme that addresses both of these problems. The main idea is to close off the coercer's window of opportunity by ensuring that the voters only learn their tracker numbers after votes have been posted. Notification of the trackers must provide high assurance but be deniable. The resulting scheme provides receipt-freeness but also provides a more immediately understandable form of verifiability: voters can find their vote, in the clear, in the tally identified by their secret tracker.

However, there is a sting in the tail: a coerced voter might light on the coercer's tracker, or the coercer may simply claim that the tracker is his. I describe some elaborations of the basic scheme to counter this problem.

http://eprint.iacr.org/2015/1105.pdf

Bio:
Peter Ryan is Professor of Applied Security at the University of Luxembourg since Feb 2009. He has around 25 years of experience in cryptography, information assurance and formal verification. He was a pioneer of the application of process calculi to modelling and analysis of secure systems, in particular to the characterization of information flows (non-interference) and the application of process algebra (CSP) and model-checking tools (FDR) to the analysis of security protocols. He has published extensively on cryptographic protocols, security policies, mathematical models of computer security and, most recently, end-to-end verifiable election systems. He is the creator of the (polling station) Prêt à Voter and, with V. Teague, the (internet) Pretty Good Democracy verifiable voting schemes. He was also co-designer of the vVote system, based on Prêt à Voter that was used successfully for Lower House elections in Victoria State, Australia in November 2014. With Feng Hao, he also developed the OpenVote boardroom voting scheme and the J-PAKE password based authenticated key establishment protocol. Recently he co-authored the “Remark!” scheme for secure, anonymous marking of exams and has been working on Quantum Authenticated Key Establishment Protocols.

Activity: Talk
Time: Tuesday May 31, 13:30
Location: Room 8103
Speaker: Gilles Barthe (IMDEA)
Title: Verification of differential private computations
Abstract:
Differential privacy is a statistical notion of privacy which achieves compelling trade-offs between input privacy and accuracy (of outputs). Differential privacy is also an attractive target for verification: despite their apparent simplicity, recently proposed algorithms have intricate privacy and accuracy proofs. We present two program logics for reasoning about privacy and accuracy properties of probabilistic computations. The accuracy logic captures reasoning about the union bound, a simple but effective tool from probablility theory, whereas the privacy logic captures fine-grained reasoning about probabilistic couplings, a powerful tool for studying Markov chains. We illustrate the strengths of our program logics with novel and elegant proofs of challenging examples from differential privacy.

Activity: Talk
Time: Friday May 27, 10:00
Location: Room 3364
Speaker: Mark S. Miller (Google)
Title: Frozen Realms: draft standard support for safer JavaScript plugins
Abstract:
Support ultra-fine-grain protection domains in JavaScript. Minimizing standardization, development, explanation, and runtime costs. Maximizing security, compatibility, simplicity, and expressiveness benefits. See https://github.com/FUDCo/proposal-frozen-realms

Bio:
Mark S. Miller is the main designer of the E and Dr. SES distributed object-capability programming languages, inventor of Miller Columns, a pioneer of agoric (market-based secure distributed) computing, an architect of the Xanadu hypertext publishing system, a representative to the EcmaScript committee, and one of Yedalog’s creators.

Activity: Talk
Time: Friday May 20, 11:00
Location: Room 3364
Speaker: Aljoscha Lautenbach
Title: A Risk Assessment Framework for Automotive Embedded Systems
Abstract:
The automotive industry is experiencing a paradigm shift towards autonomous and connected vehicles. Coupled with the increasing usage and complexity of electrical and/or electronic systems, this introduces new safety and security risks. Encouragingly, the automotive industry has relatively well-known and standardised safety risk management practices, but security risk management is still in its infancy. In order to facilitate the derivation of security requirements and security measures for automotive embedded systems, we propose a specifically tailored risk assessment framework, and we demonstrate its viability with an industry use-case. Some of the key features are alignment with existing processes for functional safety, and usability for non-security specialists.

The framework begins with a threat analysis to identify the assets, and threats to those assets. The following risk assessment process consists of an estimation of the threat level and of the impact level. This step utilises several existing standards and methodologies, with changes where necessary. Finally, a security level is estimated which is used to formulate high-level security requirements. The strong alignment with existing standards and processes should make this framework well-suited for the needs in the automotive industry.

Activity: Guest Lecture
Time: Wednesday May 11, 14:15
Location: Room ED
Speaker: Steven Van Acker
Title: Security of login pages on the Web: who else can know your password?
Abstract:
Most people with an online presence these days, store large amounts of information about their lives in online web services: e-mails, pictures, medical information, ... To prevent unauthorised access to their personal and private information, these web services require users to authenticate and this authentication is typically done using a username and password, transmitted for verification via a login page. These login pages are critical to a user’s security. If an attacker can steal a user's username and password, they can gain access to that user's account easily.

In this talk we take a look at the state of the art when it comes to security of login pages. We consider several attacker models, ranging from your typical Starbucks network attacker to sophisticated nation-state attackers.

With these attackers in mind, we look at what the ideal login page looks like, using all security measures currently built into browsers, on top of some common sense.

Once we know what the ideal login page looks like, we also take a look at real login pages on the Web. We analysed the login pages found on the top 100,000 most popular Internet domains and (responsibly) attacked them using simulated attacker models.

Beware: This data is part of ongoing research and the results may shock you. You may never wish to use the Web again!

Activity: Talk
Time: Friday May 6, 11:00
Location: Room 8103
Speaker: Gustavo Grieco (CIFASIS - CONICET and VERIMAG)
Title: Program behavior-based fuzzing and vulnerability discovery
Abstract:
Mutational fuzzing is a powerful tool to detect vulnerabilities in software. It requires a initial set of inputs for the program to test. A traditional criteria to select inputs is to maximize code coverage in order to try to use all the instructions at least once. Unfortunately it is still insufficient to deal with real-world code like complex parsers in order to discover vulnerable conditions.

In this talk we introduce a new approach based on program behaviors, in which traces are extracted and analyzed using Machine Learning to detect similarity between executions. Using this approach, we show how to perform vulnerability detection as well as preliminary results on how to improve seed selection for mutational fuzzing.

Activity: Guest Lecture
Time: Wednesday April 27, 14:15
Location: Room ED
Speaker: Aslan Askarov (Aarhus University)
Title: Architectural requirements for language-level control of external timing channels
Abstract:
A promising new approach to controlling timing channels relies on distinguishing between the direct timing dependencies that are visible at the program control flow level, and the indirect timing dependencies that typically have architectural nature. The approach allows using programming language techniques to mitigate direct dependencies, while delegating the control of the indirect dependencies to the underlying hardware. An essential element in this approach is the so-called semantic interface that stipulates a set of security and functional requirements on hardware in order for the PL-level mitigation to be sound. This talk will present the semantic interface; discuss existing practical realizations from literature, and evaluate security of this approach in a setting of active adversaries that are capable to evict caches.

Activity: Talk
Time: Friday April 22, 11:00
Location: Room 8103
Speaker: Alejandro Russo
Title: Two Can Keep a Secret, If One of Them Uses Haskell
Abstract:
For several decades, researchers from different communities have independently focused on protecting confidentiality of data. Two distinct technologies have emerged for such purposes: Mandatory Access Control (MAC) and Information-Flow Control (IFC)—the former belonging to operating systems (OS) research, while the latter to the programming languages community. These approaches restrict how data gets propagated within a system in order to avoid information leaks. In this scenario, the functional programming language Haskell plays a unique privileged role: it is able to protect confidentiality via libraries. This talk presents an (monadic) API which statically protects confidentiality even in the presence of advanced features like exceptions, concurrency, and mutable data structures.

This talk is based on the paper "Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell" presented in ICFP 2015.

Activity: General Talk
Time: Friday April 1, 11:00
Location: Room 8103
Speaker: Elena Pagnin
Title: Recent Breakthroughs in Program Obfuscation
Abstract:
This talk is supposed to give an overview of the state of the art in the area of Homomorphic Encryption (HE) and Multi-Linear Maps (MLM). The final section of the talk will deal with the definition and application of indistinguishable Obfuscation.

More precisely, I will recall the syntax of FHE schemes and provide a trivial (extremely inefficient) construction of a FHE scheme. I will then cite the most significant papers in the area, highlight the trend and evolution of FHE schemes over the years (since Gentry’s first construction in 2009) and finally conclude with a slide that shows the timing required to perform homomorphic operations on a FHE scheme implemented by Halevi.

The main focus of the talk is on Muliti-Linear Maps (MLM). Roughly speaking, MLMs can be thought of as a FHE scheme in which there is no decryption, but it is possible to check if two (top level) cipher-texts are equal or not. This latter property is called zero testing and it is the main feature, but also weakness, of MLMs. I will present the second MLM candidate, the CLT13, which is based on relatively easy mathematical tools (congruences and Chinese Remainder Theorem), and its cryptanalysis (zeroing attack).

The talk will end with an introduction to obfuscation. From an abstract point of view, one could think at obfuscation as a MLM without zero testing and in which only a pre-determined sequence of operations is allowed. In practice, an obfuscator is an algorithm that takes as input a program P and outputs another program O(P). such that O(P) and P have equal outputs on equal inputs and O(P) is an intelligible program.

Activity: Talk
Time: Thursday March 17, 13:30
Location: Room 3364
Speaker: Matteo Maffei
Title: Formal Security Analysis of Mobile and Web Applications
Abstract:
In this talk, I will present two ongoing projects on the formal verification of security properties for mobile and web applications.

In the first part, I will present HornDroid, a novel technique for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by SMT solving. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still relying on off-the-shelf verification tools, thereby automatically leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms in precision state-of-the-art Android static analysis tools on benchmarks proposed by the community, besides being orders of magnitude faster. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness: besides yielding correctness assurances, this proof allowed us to identify some critical corner-cases that affect the soundness guarantees provided by some of the previous static analysis tools for Android.

In the second part, I will present Michrome, a security enforcement tool for web applications based on micro-policies. Micro-policies, originally proposed to implement hardware-level security monitors, constitute a flexible and general enforcement technique, based on assigning security tags to system components and taking security actions based on dynamic checks over these tags. In this work, we present the first application of micro-policies to web security, by proposing a core browser model supporting them and studying its effectiveness at securing web sessions. In our view, web session security requirements are expressed in terms of a simple, purely declarative information flow policy, which is then automatically translated into a micro-policy implementing it. This leads to a browser-side enforcement mechanism which is elegant, sound and flexible, while being accessible to web developers. We show how a large class of attacks against web sessions can be uniformly and effectively prevented by the adoption of this approach. Since we carefully designed micro-policies with ease of deployment in mind, we are also able to implement our proposal as a Google Chrome extension, Michrome: our experiments show that Michrome can be easily configured to enforce strong security policies without breaking the websites functionality.
Bio:
Matteo Maffei is professor at Saarland University and CISPA, where he leads the Secure and Privacy-preserving Systems group. He received his Ph.D. in Computer Science from the University of Venice in 2006. Matteo’s research interests are in the area of formal methods for security analysis, with a focus on cryptographic protocols, mobile security, and web security, as well as privacy-enhancing technologies, in particular zero-knowledge proofs, oblivious RAM, and differential privacy. He was granted the Emmy Noether fellowship from the German research foundation in 2009, he served in the programme committee of more than 40 conferences, and he is currently the regular columnist on security and privacy of the ACM SIGLOG newsletter.

Activity: Talk
Time: Monday February 29, 10:00
Location: Room 8103
Speaker: William Robertson
Title: How to Get Away with Malware (and, How Not To)
Abstract:
The modern Web is heavily reliant on JavaScript for implementing client-side web applications and extending browser functionality. And yet, despite varied efforts to isolate, tame, or analyze it, JavaScript continues to enable new attacks against the web platform.

In this talk, I will present recent work on bypassing browser security controls via a novel form of code reuse, and discuss a lightweight static analysis to detect this class of vulnerabilities. Then, I will present ZigZag, a system for hardening JavaScript-based web applications against client-side validation vulnerabilities that relies on invariant detection and efficient instrumentation.
Bio:
William Robertson is an assistant professor of Computer Science at Northeastern University in Boston, MA, and co-directs the NEU Systems Security Lab. His research revolves around improving the security of operating systems, mobile devices, and the web, making use of techniques such as security by design, program analysis, and anomaly detection.

Activity: Kickoff meeting
Time: Thursday February 11, 15:00
Location: 8103
Summary:
The contents of the Chalmers Security Seminar was discussed and the following was agreed on.

Talks should be of the following types:
- Presentations of papers from top conferences
- Invited speakers
- Recently published papers
- Ongoing research
- "Hack-of-the-moment" talks
PhD students should be able to get credits for attending the seminars and preparing talks:
- It should be possible to join the course at any time
- Master students should be allowed to attend the seminars, however, they will not have to give talks

A website for both security groups is under construction, which was also discussed during the meeting.

Activity: Talk
Time: Thursday Januray 28, 15:00
Location: Room EA
Speaker: Prof. Lujo Bauer from Carnegie Mellon University (bio: http://www.ece.cmu.edu/~lbauer/bio.html)
Title: Towards more secure and usable text passwords
Abstract:
Many security problems arise at the interface between computer systems and their users. One set of such problems relates to authentication and text-based passwords, which despite numerous shortcomings and attacks remain the dominant authentication method in computer systems.

Is pa$$w0rd1 a good password or a bad one? For several years, we've been studying how to help users create passwords that are hard for attackers to crack, but are still easy for users to remember and use. A key challenge in this work was to develop and validate a methodology for collecting passwords and assessing their strength and usability. I'll discuss our approach, and how we applied it to over 50,000 participants to study the effects of password-composition policies, password-strength meters, and detailed, step-by-step feedback and guidance during the password creation policies.

List of Papers

Possible venues for selecting papers include, but are not limited to: CCS, CSF, PLDI, POPL, Security&Privacy and USENIX Security.

Contact Information

Please contact Musard Balliu (musard at chalmers.se) or Boel Nelson (boeln at chalmers.se) if you want to give or request a talk.