TS News

News

Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System
This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System

This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

2015-09-01 Google PhD fellowship
Congratulations to PhD student Qian Ge who has won a Google PhD fellowship with Research Proposal Title: Low Overhead Operating System Mechanisms for Eliminating Microarchitectural Timing Side Channels

Seminar 2015-08-25: Huan Nguyen on Rule-Based Extraction of Goal-Use Case Models from Text
Goal and use case modeling has been recognized as a key approach for understanding and analyzing requirements. However, in practice, goals and use cases are often buried among other content in requirements specifications documents and written in unstructured styles. It is thus a time-consuming and error-prone process to identify such goals and use cases. In addition, having them embedded in natural language documents greatly limits the possibility of formally analyzing the requirements for problems. To address these issues, we have developed a novel rule-based approach to automatically extract goal and use case models from natural language requirements documents. Our approach is able to automatically categorize goals and ensure they are properly specified. We also provide automated semantic parameterization of artifact textual specifications to promote further analysis on the extracted goal-use case models. Our approach achieves 85% precision and 82% recall rates on average for model extraction and 88% accuracy for the automated parameterization.

Seminar 2015-08-25: Huan Nguyen on Rule-Based Extraction of Goal-Use Case Models from Text

Goal and use case modeling has been recognized as a key approach for understanding and analyzing requirements. However, in practice, goals and use cases are often buried among other content in requirements specifications documents and written in unstructured styles. It is thus a time-consuming and error-prone process to identify such goals and use cases. In addition, having them embedded in natural language documents greatly limits the possibility of formally analyzing the requirements for problems. To address these issues, we have developed a novel rule-based approach to automatically extract goal and use case models from natural language requirements documents. Our approach is able to automatically categorize goals and ensure they are properly specified. We also provide automated semantic parameterization of artifact textual specifications to promote further analysis on the extracted goal-use case models. Our approach achieves 85% precision and 82% recall rates on average for model extraction and 88% accuracy for the automated parameterization.

Seminar 2015-08-20: Florian Daniel; Recommendation and Weaving of Reusable Mashup Model Patterns for Assisted Development
Mashups are composite applications developed starting from reusable data, application logic and/or user interfaces, for example, sourced from the Web. Mashup tools are IDEs for mashup development that aim to ease mashup development, typically via model-driven development paradigms. This talk reports on recent research outcomes that aim to answer one of the problems proper of the mashup domain, that is, the lack of modeling expertise. This kind of knowledge is generally neither intuitive nor standardized across different tools, and the consequent lack of modeling expertise affects both skilled programmers and end-user programmers alike. The talk shows how to effectively assist the users of mashup tools with contextual, interactive recommendations of composition knowledge in the form of reusable mashup model patterns. It describes the design and performance study of three different recommendation algorithms and a pattern weaving approach for the one-click reuse of model patterns inside model-driven mashup tools. It discusses the implementation of suitable pattern recommender plugins for three different mashup tools and demonstrates via user studies that recommending and weaving contextual mashup model patterns significantly reduces development times in all three cases. The approach is of general nature and can easily be tailored to other model-driven development environments.

Seminar 2015-08-20: Florian Daniel; Recommendation and Weaving of Reusable Mashup Model Patterns for Assisted Development

Mashups are composite applications developed starting from reusable data, application logic and/or user interfaces, for example, sourced from the Web. Mashup tools are IDEs for mashup development that aim to ease mashup development, typically via model-driven development paradigms. This talk reports on recent research outcomes that aim to answer one of the problems proper of the mashup domain, that is, the lack of modeling expertise. This kind of knowledge is generally neither intuitive nor standardized across different tools, and the consequent lack of modeling expertise affects both skilled programmers and end-user programmers alike. The talk shows how to effectively assist the users of mashup tools with contextual, interactive recommendations of composition knowledge in the form of reusable mashup model patterns. It describes the design and performance study of three different recommendation algorithms and a pattern weaving approach for the one-click reuse of model patterns inside model-driven mashup tools. It discusses the implementation of suitable pattern recommender plugins for three different mashup tools and demonstrates via user studies that recommending and weaving contextual mashup model patterns significantly reduces development times in all three cases. The approach is of general nature and can easily be tailored to other model-driven development environments.

Seminar;2015-08-19: Gorka Irazoqui on Prevention of microarchitectural side channel attacks in the cloud
Side channel attacks have shown to be a potential thread for co-resident virtual machines in cloud computing environments. Among all, last level cache side channel attacks have proved to be the most powerful ones, being able to extract fine grain information such as cryptographic keys. Due to the increasing success of these kind of attacks, protections have to be implemented against them. In this work, we are building a tool that can mitigate side channel attacks in cloud environments. This is implemented in two steps: first, an identification phase where we detect that a malicious VM is running a side channel attack, and second, mitigate the attack by changing the memory layout of the malicious VM. For the identification phase, Hardware Performance Counters will be analysed looking for expected patterns for cache side channel attacks. In the mitigation phase, we will move malicious VM's memory pages to form a moving target defence. Although the tool will be applied to detect cache based side channel attacks, we believe it could also be adapted to detect microarchitectural attacks that use different hardware resources. This is work in progress.

Seminar;2015-08-19: Gorka Irazoqui on Prevention of microarchitectural side channel attacks in the cloud

Side channel attacks have shown to be a potential thread for co-resident virtual machines in cloud computing environments. Among all, last level cache side channel attacks have proved to be the most powerful ones, being able to extract fine grain information such as cryptographic keys. Due to the increasing success of these kind of attacks, protections have to be implemented against them. In this work, we are building a tool that can mitigate side channel attacks in cloud environments. This is implemented in two steps: first, an identification phase where we detect that a malicious VM is running a side channel attack, and second, mitigate the attack by changing the memory layout of the malicious VM. For the identification phase, Hardware Performance Counters will be analysed looking for expected patterns for cache side channel attacks. In the mitigation phase, we will move malicious VM's memory pages to form a moving target defence. Although the tool will be applied to detect cache based side channel attacks, we believe it could also be adapted to detect microarchitectural attacks that use different hardware resources. This is work in progress.

Show older articles

Trustworthy Systems

News