Recent Changes - Search:
ST /

STWinterMeeting2016

"Vintermötet" = ST Winter Meeting 2016

History: ST Winter Meeting 2015, ST Winter Meeting 2014, ... ST Winter Meeting History

The winter meeting will be held at Bokenäs Hav Spa on the 2nd-3rd of February. As usual, there will be talks as well as social activities. We recommend taking bathing suits as Bokenäs has spa facilities and a flashlight for walks.

Getting there

Bus leaves from Copper Dome (Kopparbunkern) Driving

Detailed schedule

Day 1 (= Tue)

  • 8:00 Bus leaving Chalmers
  • ~9:20-9.50 Arrival Bokenäs Hav Spa, Coffe/Tea
  • 9.50-10.00 Welcome
  • 10:00-12:00 Session 1 (Session chair: Gerardo Schneider)
  • 12.00-13.30 Lunch
  • 13:30-15:30 Long term planning (Patrik Jansson)
  • 15:30-16:00 Coffe
  • 16.00-17.00 Session 2 (Session chair: Wolfgang Arendt)
  • 17:00-19:30 Activity
  • 19:30 Dinner

Day 2 (= Wed)

Organizing team: Tiina Rankanen, Joachim von Hacht, Jonas Duregård, Josef Svenningsson

Abstracts

Solving Linear Integer Constraints by Translation into SAT

I will present a completely new method for solving linear constraints over integers (ILP), that translates the given problem into a SAT problem. The new method thus avoids the explicit and expensive backtracking that is an integral part of most ILP solving methods, and instead makes use of the efficient search procedure that is built-in into a SAT-solver. The method is based on the well-known Omega Test, but is a lot simpler, both for understanding by humans and to implement. The method can be seemlessly integrated into an SMT-solver.

"An extensible information-flow library for external effects"

Existing Information flow tracking tools typically handle a fixed set of effects baked in the tool itself, therefore when used in practice they often need to be extended. Unfortunately these extensions are usually ad-hoc and require security experts knowledge.

We present a calculus to systematically extend IFC languages with external effects and resources, such as references, file systems, email servers. Our technique is based on two well-known principles (no read-up and no write-down), traditionally employed in operative systems as Mandatory Access Control (MAC) mechanisms. We demonstrate this technique in a Haskell library, in which developers only need to specify the read and write effects of new primitives. We have formalised the calculus in Agda and proved that it satisfies termination insensitive non-interference.

"Musings from the new IT program responsible"

From January 1st I have replaced Wolfgang as the new head of the IT program. I would like to take the opportunity to present ongoing changes to the program, as well as some future plans and grand visions, and welcome your input and suggestions.

“What good are formal specifications?”

A high-level overview of my research in verification and dynamic analysis, with focus on the underlying idea of taking advantage of simple functional formal specifications to make formal methods (somewhat) more applicable in practice on realistic programs.

"Loops Fall Apart When One Pulls The Zipper"

Implementation of collection traversal as traversal of its subcollections is a transformation commonly used in scheduling for parallel execution and in optimizing the memory bandwidth utilization. In an imperative language such an implementation is often a nested loop. I demonstrate that in a functional language an equivalent concept is a pair of mutually tail-recursive functions which can be translated to an equivalent imperative nested loop. I will also show that if a collection datatype is a Huet zipper, optimized implementation of its traversal can be derived from the traversal definition mechanically using Dagand-McBride function ornaments.

"Imperative Embedded Languages"

I will give a small tutorial of using the imperative-edsl package. Making your own EDSL for generating C code has never been easier!

“Evolving Privacy Policies for Social Networks”

Protecting users privacy in Social Network Sites (SNS) is a challenging issue. The privacy policies that SNSs offer today are focused on *what* information is accessible to *whom*. However, there are other factors that can be considered for privacy policies, for instance, *when* the privacy policies must be enforced or *how* (for which purpose) the information can be accessed. In this talk, I will present a novel approach to enforcing privacy policies which are regarded to *when* the private information of a user can be accessed. For example, a user is be able to write a policy saying "My boss cannot see the pictures I am tagged in from Friday at 18:00 to Monday 8:00" or "Nobody can know my location more than 3 times per day". In order model evolving privacy policies we introduce the notion of policy automata, which is a an automaton where transitions can be triggered by events in the SNS or timers, and states describe the set of privacy policies to be enforced. As a proof-of-concept we have implemented some examples of evolving policies in the open source SNS Diaspora*, and we have used the tool LARVA to automatically generate the corresponding automata for each privacy policy.

“Data Exfiltration in the Face of CSP”

Cross-site scripting (XSS) attacks keep plaguing the Web. Supported by most modern browsers, Content Security Policy (CSP) prescribes the browser to restrict the features and communication capabilities of code on a web page, mitigating the effects of XSS. This paper puts a spotlight on the problem of data exfiltration in the face of CSP. We bring attention to the unsettling discord in the security community about the very goals of CSP when it comes to preventing data leaks. As consequences of this discord, we report on insecurities in the known protection mechanisms that are based on assumptions about CSP that turn out not to hold in practice. To illustrate the practical impact of the discord, we perform a systematic case study of data exfiltration via DNS prefetching and resource prefetching in the face of CSP.

Our study of the popular browsers demonstrates that it is often possible to exfiltrate data by both resource prefetching and DNS prefetching in the face of CSP. Further, we perform a crawl of the top 10,000 Alexa domains to report on the cohabitance of CSP and prefetching in practice. Finally, we discuss directions to control data exfiltration and, for the case study, propose measures ranging from immediate fixes for the clients to prefetching-aware extensions of CSP.

"On Security of Browser Extensions"

Browser extensions enrich user experience, as e.g. witnessed by tens of thousands extensions available in Chrome's web store. However, browser extensions also introduce significant security risks, being de-facto a man-in-the-middle between the user's browser and the web. This talk describes some insights from an empirical study with all free extensions from Chrome's web store (around 30,000) that demonstrate clashes of security goals of the web pages and the browser.

"Faceted Values for Taint Tracking"

Taint tracking has been successfully deployed in a range of security applications to track data dependencies in hardware and machine-, binary-, and high-level code. Precision of taint tracking is key for its usage in practice: being a vulnerability analysis, false positives must be minimal for the analysis to have a chance to be practical. This paper presents an approach to taint tracking, which does not involve tracking taints throughout computation. Instead, we include shadow memories in the execution context, so that a single run of a program has the effect of computing on both tainted and untainted data. This mechanism is inspired by the technique of secure multi-execution, while in contrast to the latter it does not require running the program multiple times. We present a general framework and establish its soundness with respect to explicit secrecy, a policy for preventing insecure data leaks. We show that the technique can be used for attack detection with no false positives. We implement the approach by a source-to-source transform for a core of Java and benchmark its precision and performance with respect to FlowDroid and TaintDroid, typical representatives of static and dynamic taint tracking for Java, respectively.