-
Friend or Foe Inside? Exploring In-Process Isolation to Maintain Memory Safety for Unsafe Rust
Authors:
Merve Gülmez,
Thomas Nyman,
Christoph Baumann,
Jan Tobias Mühlberg
Abstract:
Rust is a popular memory-safe systems programming language. In order to interact with hardware or call into non-Rust libraries, Rust provides \emph{unsafe} language features that shift responsibility for ensuring memory safety to the developer. Failing to do so, may lead to memory safety violations in unsafe code which can violate safety of the entire application. In this work we explore in-proces…
▽ More
Rust is a popular memory-safe systems programming language. In order to interact with hardware or call into non-Rust libraries, Rust provides \emph{unsafe} language features that shift responsibility for ensuring memory safety to the developer. Failing to do so, may lead to memory safety violations in unsafe code which can violate safety of the entire application. In this work we explore in-process isolation with Memory Protection Keys as a mechanism to shield safe program sections from safety violations that may happen in unsafe sections. Our approach is easy to use and comprehensive as it prevents heap and stack-based violations. We further compare process-based and in-process isolation mechanisms and the necessary requirements for data serialization, communication, and context switching. Our results show that in-process isolation can be effective and efficient, permits for a high degree of automation, and also enables a notion of application rewinding where the safe program section may detect and safely handle violations in unsafe code.
△ Less
Submitted 13 June, 2023;
originally announced June 2023.
-
Exploring the Environmental Benefits of In-Process Isolation for Software Resilience
Authors:
Merve Gülmez,
Thomas Nyman,
Christoph Baumann,
Jan Tobias Mühlberg
Abstract:
Memory-related errors remain an important cause of software vulnerabilities. While mitigation techniques such as using memory-safe languages are promising solutions, these do not address software resilience and availability. In this paper, we propose a solution to build resilience against memory attacks into software, which contributes to environmental sustainability and security.
Memory-related errors remain an important cause of software vulnerabilities. While mitigation techniques such as using memory-safe languages are promising solutions, these do not address software resilience and availability. In this paper, we propose a solution to build resilience against memory attacks into software, which contributes to environmental sustainability and security.
△ Less
Submitted 3 June, 2023;
originally announced June 2023.
-
End-to-End Security for Distributed Event-Driven Enclave Applications on Heterogeneous TEEs
Authors:
Gianluca Scopelliti,
Sepideh Pouyanrad,
Job Noorman,
Fritz Alder,
Christoph Baumann,
Frank Piessens,
Jan Tobias Mühlberg
Abstract:
This paper presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Trusted Computing Base. We build upon and extend security primitives provided by Trusted Execution Environments (TEEs) to guarantee authenticity and integrity properties of applications, and to secure control of input and o…
▽ More
This paper presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Trusted Computing Base. We build upon and extend security primitives provided by Trusted Execution Environments (TEEs) to guarantee authenticity and integrity properties of applications, and to secure control of input and output devices. More specifically, we guarantee that if an output is produced by the application, it was allowed to be produced by the application's source code based on an authentic trace of inputs.
We present an integrated open-source framework to develop, deploy, and use such applications across heterogeneous TEEs. Beyond authenticity and integrity, our framework optionally provides confidentiality and a notion of availability, and facilitates software development at a high level of abstraction over the platform-specific TEE layer. We support event-driven programming to develop distributed enclave applications in Rust and C for heterogeneous TEE, including Intel SGX, ARM TrustZone and Sancus.
In this article we discuss the workings of our approach, the extensions we made to the Sancus processor, and the integration of our development model with commercial TEEs. Our evaluation of security and performance aspects show that TEEs, together with our programming model, form a basis for powerful security architectures for dependable systems in domains such as Industrial Control Systems and the Internet of Things, illustrating our framework's unique suitability for a broad range of use cases which combine cloud processing, mobile and edge devices, and lightweight sensing and actuation.
△ Less
Submitted 29 June, 2023; v1 submitted 2 June, 2022;
originally announced June 2022.
-
Unlimited Lives: Secure In-Process Rollback with Isolated Domains
Authors:
Merve Gülmez,
Thomas Nyman,
Christoph Baumann,
Jan Tobias Mühlberg
Abstract:
The use of unsafe programming languages still remains one of the major root causes of software vulnerabilities. Although well-known defenses that detect and mitigate memory-safety related issues exist, they don't address the challenge of software resilience, i.e., whether a system under attack can continue to carry out its function when subjected to malicious input. We propose secure rollback of i…
▽ More
The use of unsafe programming languages still remains one of the major root causes of software vulnerabilities. Although well-known defenses that detect and mitigate memory-safety related issues exist, they don't address the challenge of software resilience, i.e., whether a system under attack can continue to carry out its function when subjected to malicious input. We propose secure rollback of isolated domains as an efficient and secure method of improving the resilience of software targeted by run-time attacks. We show the practicability of our methodology by realizing a software library for Secure Domain Rollback (SDRoB) and demonstrate how SDRoB can be applied to real-world software.
△ Less
Submitted 21 April, 2023; v1 submitted 6 May, 2022;
originally announced May 2022.
-
Data-driven control of room temperature and bidirectional EV charging using deep reinforcement learning: simulations and experiments
Authors:
B. Svetozarevic,
C. Baumann,
S. Muntwiler,
L. Di Natale,
M. Zeilinger,
P. Heer
Abstract:
This work presents a fully data-driven, black-box pipeline to obtain an optimal control policy for a multi-loop building control problem based on historical building and weather data, thus without the need for complex physics-based modelling. We demonstrate the method for joint control of room temperature and bidirectional EV charging to maximize the occupant thermal comfort and energy savings whi…
▽ More
This work presents a fully data-driven, black-box pipeline to obtain an optimal control policy for a multi-loop building control problem based on historical building and weather data, thus without the need for complex physics-based modelling. We demonstrate the method for joint control of room temperature and bidirectional EV charging to maximize the occupant thermal comfort and energy savings while leaving enough energy in the EV battery for the next trip. We modelled the room temperature with a recurrent neural network and EV charging with a piece-wise linear function. Using these models as a simulation environment, we applied a deep reinforcement learning (DRL) algorithm to obtain an optimal control policy. The learnt policy achieves on average 17% energy savings over the heating season and 19% better comfort satisfaction than a standard RB room temperature controller. When a bidirectional EV is additionally connected and a two-tariff electricity pricing is applied, the MIMO DRL policy successfully leverages the battery and decreases the overall cost of electricity compared to two standard RB controllers, one controlling the room temperature and another controlling the bidirectional EV (dis-)charging. Finally, we demonstrate a successful transfer of the learnt DRL policy from simulation onto a real building, the DFAB HOUSE at Empa Duebendorf in Switzerland, achieving up to 30% energy savings while maintaining similar comfort levels compared to a conventional RB room temperature controller over three weeks during the heating season.
△ Less
Submitted 17 June, 2021; v1 submitted 2 March, 2021;
originally announced March 2021.
-
A High-Level Description and Performance Evaluation of Pupil Invisible
Authors:
Marc Tonsen,
Chris Kay Baumann,
Kai Dierkes
Abstract:
Head-mounted eye trackers promise convenient access to reliable gaze data in unconstrained environments. Due to several limitations, however, often they can only partially deliver on this promise.
Among those are the following: (i) the necessity of performing a device setup and calibration prior to every use of the eye tracker, (ii) a lack of robustness of gaze-estimation results against perturb…
▽ More
Head-mounted eye trackers promise convenient access to reliable gaze data in unconstrained environments. Due to several limitations, however, often they can only partially deliver on this promise.
Among those are the following: (i) the necessity of performing a device setup and calibration prior to every use of the eye tracker, (ii) a lack of robustness of gaze-estimation results against perturbations, such as outdoor lighting conditions and unavoidable slippage of the eye tracker on the head of the subject, and (iii) behavioral distortion resulting from social awkwardness, due to the unnatural appearance of current head-mounted eye trackers.
Recently, Pupil Labs released Pupil Invisible glasses, a head-mounted eye tracker engineered to tackle these limitations. Here, we present an extensive evaluation of its gaze-estimation capabilities. To this end, we designed a data-collection protocol and evaluation scheme geared towards providing a faithful portrayal of the real-world usage of Pupil Invisible glasses.
In particular, we develop a geometric framework for gauging gaze-estimation accuracy that goes beyond reporting mean angular accuracy. We demonstrate that Pupil Invisible glasses, without the need of a calibration, provide gaze estimates which are robust to perturbations, including outdoor lighting conditions and slippage of the headset.
△ Less
Submitted 1 September, 2020;
originally announced September 2020.
-
Lessons Learned From Microkernel Verification -- Specification is the New Bottleneck
Authors:
Christoph Baumann,
Bernhard Beckert,
Holger Blasum,
Thorsten Bormer
Abstract:
Software verification tools have become a lot more powerful in recent years. Even verification of large, complex systems is feasible, as demonstrated in the L4.verified and Verisoft XT projects. Still, functional verification of large software systems is rare - for reasons beyond the large scale of verification effort needed due to the size alone. In this paper we report on lessons learned for…
▽ More
Software verification tools have become a lot more powerful in recent years. Even verification of large, complex systems is feasible, as demonstrated in the L4.verified and Verisoft XT projects. Still, functional verification of large software systems is rare - for reasons beyond the large scale of verification effort needed due to the size alone. In this paper we report on lessons learned for verification of large software systems based on the experience gained in microkernel verification in the Verisoft XT project. We discuss a number of issues that impede widespread introduction of formal verification in the software life-cycle process.
△ Less
Submitted 26 November, 2012;
originally announced November 2012.
