Showing 1–10 of 10 results for author: Balzer, S

Information Flow Control in Cyclic Process Networks

Authors: Bas van den Heuvel, Farzaneh Derakhshan, Stephanie Balzer

Abstract: Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC ty… ▽ More Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today's applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work. △ Less

Submitted 2 July, 2024; originally announced July 2024.

Comments: Extended version of ECOOP24 paper

M(otion)-mode Based Prediction of Ejection Fraction using Echocardiograms

Authors: Ece Ozkan, Thomas M. Sutter, Yurong Hu, Sebastian Balzer, Julia E. Vogt

Abstract: Early detection of cardiac dysfunction through routine screening is vital for diagnosing cardiovascular diseases. An important metric of cardiac function is the left ventricular ejection fraction (EF), where lower EF is associated with cardiomyopathy. Echocardiography is a popular diagnostic tool in cardiology, with ultrasound being a low-cost, real-time, and non-ionizing technology. However, huma… ▽ More Early detection of cardiac dysfunction through routine screening is vital for diagnosing cardiovascular diseases. An important metric of cardiac function is the left ventricular ejection fraction (EF), where lower EF is associated with cardiomyopathy. Echocardiography is a popular diagnostic tool in cardiology, with ultrasound being a low-cost, real-time, and non-ionizing technology. However, human assessment of echocardiograms for calculating EF is time-consuming and expertise-demanding, raising the need for an automated approach. In this work, we propose using the M(otion)-mode of echocardiograms for estimating the EF and classifying cardiomyopathy. We generate multiple artificial M-mode images from a single echocardiogram and combine them using off-the-shelf model architectures. Additionally, we extend contrastive learning (CL) to cardiac imaging to learn meaningful representations from exploiting structures in unlabeled data allowing the model to achieve high accuracy, even with limited annotations. Our experiments show that the supervised setting converges with only ten modes and is comparable to the baseline method while bypassing its cumbersome training process and being computationally much more efficient. Furthermore, CL using M-mode images is helpful for limited data scenarios, such as having labels for only 200 patients, which is common in medical applications. △ Less

Submitted 7 September, 2023; originally announced September 2023.

Comments: Accepted at GCPR 2023

Logical Relations for Session-Typed Concurrency

Authors: Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao

Abstract: Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types -- but exclusively for terminating languages. This paper scales logical relations to… ▽ More Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types -- but exclusively for terminating languages. This paper scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive noninterference (PSNI) for intuitionistic linear logic session types (ILLST), tackling the challenges non-termination and concurrency pose, and shows that logical equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition, using a biorthogonality argument. A distinguishing feature of the logical relation is its stratification with an observation index (as opposed to a step or unfolding index), a crucial shift to make the logical relation closed under parallel composition in a concurrent setting. To demonstrate practicality of the logical relation, the paper develops an information flow control (IFC) refinement type system for ILLST, with support of secrecy-polymorphic processes, and shows that well-typed programs are self-related by the logical relation and thus enjoy PSNI. The refinement type system has been implemented in a type checker, featuring local security theories to support secrecy-polymorphic processes. △ Less

Submitted 31 August, 2023; originally announced September 2023.

Comments: arXiv admin note: text overlap with arXiv:2208.13741

Recursive Session Logical Relations

Authors: Farzaneh Derakhshan, Stephanie Balzer

Abstract: Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types--but exclusively for terminating languages. This paper scales logical relations to re… ▽ More Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types--but exclusively for terminating languages. This paper scales logical relations to recursive session types. It develops a logical relation for progress-sensitive noninterference for linear session types, tackling the challenges non-termination and concurrency pose. The contributions include secrecy-polymorphic processes and the logical relation with metatheory. A distinguishing feature is the choice of "step index" of the logical relation, allowing for a natural proof of transitivity and soundness. △ Less

Submitted 30 August, 2022; v1 submitted 29 August, 2022; originally announced August 2022.

Ferrite: A Judgmental Embedding of Session Types in Rust

Authors: Ruo Fei Chen, Stephanie Balzer, Bernardo Toninho

Abstract: \emph{Session types} have proved viable in expressing and verifying the protocols of message-passing systems. While message passing is a dominant concurrency paradigm in practice, real world software is written without session types. A limitation of existing session type libraries in mainstream languages is their restriction to linear session types, precluding application scenarios that demand sha… ▽ More \emph{Session types} have proved viable in expressing and verifying the protocols of message-passing systems. While message passing is a dominant concurrency paradigm in practice, real world software is written without session types. A limitation of existing session type libraries in mainstream languages is their restriction to linear session types, precluding application scenarios that demand sharing and thus aliasing of channel references. This paper introduces Ferrite, a shallow embedding of session types in Rust that supports both \emph{linear} and \emph{shared} sessions. The formal foundation of Ferrite constitutes the shared session type calculus $\sills$, which Ferrite encodes via a novel \emph{judgmental embedding} technique. The fulcrum of the embedding is the notion of a typing judgment that allows reasoning about shared and linear resources to type a session. Typing rules are then encoded as functions over judgments, with a valid typing derivation manifesting as a well-typed Rust program. This Rust program generated by Ferrite serves as a \emph{certificate}, ensuring that the application will proceed according to the protocol defined by the session type. The paper details the features and implementation of Ferrite and includes a case study on implementing Servo's canvas component in Ferrite. △ Less

Submitted 31 May, 2022; v1 submitted 13 May, 2022; originally announced May 2022.

Comments: Accidental duplication of arXiv:2009.13619

Session Logical Relations for Noninterference

Authors: Farzaneh Derakhshan, Stephanie Balzer, Limin Jia

Abstract: Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asserting that an attacker cannot infer any secrets from made observations. Session types delimit the kinds of observations that can be made along a communication channel by imposing a protocol of message exchange. These prot… ▽ More Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asserting that an attacker cannot infer any secrets from made observations. Session types delimit the kinds of observations that can be made along a communication channel by imposing a protocol of message exchange. These protocols govern the exchange along a single channel and leave unconstrained the propagation along adjacent channels. This paper contributes an information flow control type system for linear session types. The type system stands in close correspondence with intuitionistic linear logic. Intuitionistic linear logic typing ensures that process configurations form a tree such that client processes are parent nodes and provider processes child nodes. To control the propagation of secret messages, the type system is enriched with secrecy levels and arranges these levels to be aligned with the configuration tree. Two levels are associated with every process: the maximal secrecy denoting the process' security clearance and the running secrecy denoting the highest level of secret information obtained so far. The computational semantics naturally stratifies process configurations such that higher-secrecy processes are parents of lower-secrecy ones, an invariant enforced by typing. Noninterference is stated in terms of a logical relation that is indexed by the secrecy-level-enriched session types. The logical relation contributes a novel development of logical relations for session typed languages as it considers open configurations, allowing for more nuanced equivalence statement. △ Less

Submitted 28 April, 2021; originally announced April 2021.

Manifestly Phased Communication via Shared Session Types

Authors: Chuta Sano, Stephanie Balzer, Frank Pfenning

Abstract: Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this pap… ▽ More Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client. △ Less

Submitted 26 November, 2021; v1 submitted 15 January, 2021; originally announced January 2021.

Comments: Extended and revised version of a paper presented at COORDINATION 2021

Ferrite: A Judgmental Embedding of Session Types in Rust

Authors: Ruofei Chen, Stephanie Balzer, Bernardo Toninho

Abstract: This paper introduces Ferrite, a shallow embedding of session types in Rust. In contrast to existing session type libraries and embeddings for mainstream languages, Ferrite not only supports linear session types but also shared session types. Shared session types allow sharing (aliasing) of channels while preserving session fidelity (preservation) using type modalities for acquiring and releasing… ▽ More This paper introduces Ferrite, a shallow embedding of session types in Rust. In contrast to existing session type libraries and embeddings for mainstream languages, Ferrite not only supports linear session types but also shared session types. Shared session types allow sharing (aliasing) of channels while preserving session fidelity (preservation) using type modalities for acquiring and releasing sessions. Ferrite adopts a propositions as types approach and encodes typing derivations as Rust functions, with the proof of successful type-checking manifesting as a Rust program. We provide an evaluation of Ferrite using Servo as a practical example, and demonstrate how safe communication can be achieved in the canvas component using Ferrite. △ Less

Submitted 31 May, 2022; v1 submitted 28 September, 2020; originally announced September 2020.

Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software

Authors: Stephanie Balzer, Luca Padovani

Abstract: Modern hardware platforms, from the very small to the very large, increasingly provide parallel and distributed computing resources for applications to maximise performance. Many applications therefore need to make effective use of tens, hundreds, and even thousands of compute nodes. Computation in such systems is thus inherently concurrent and communication centric. Effectively programming such a… ▽ More Modern hardware platforms, from the very small to the very large, increasingly provide parallel and distributed computing resources for applications to maximise performance. Many applications therefore need to make effective use of tens, hundreds, and even thousands of compute nodes. Computation in such systems is thus inherently concurrent and communication centric. Effectively programming such applications is challenging; performance, correctness, and scalability are difficult to achieve. The development of effective programming methodologies for this increasingly parallel landscape therefore demands exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. This volume contains the proceedings of the 12th edition of PLACES, which was co-located with ETAPS 2020 in Dublin, Ireland. △ Less

Submitted 1 April, 2020; originally announced April 2020.

Journal ref: EPTCS 314, 2020

Resource-Aware Session Types for Digital Contracts

Authors: Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar

Abstract: Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and… ▽ More Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nomos uses a linear type system. A monad integrates the effectful session-typed language with a general-purpose functional language. Nomos' prototype implementation features linear-time type checking and efficient type reconstruction that includes automatic inference of resource bounds via off-the-shelf linear optimization. The effectiveness of the language is evaluated with case studies about implementing common smart contracts such as auctions, elections, and currencies. Nomos is completely formalized, including the type system, a cost semantics, and a transactional semantics to instantiate Nomos contracts on a blockchain. The type soundness proof ensures that protocols are followed at run-time and that types establish sound upper bounds on the resource consumption, ruling out re-entrancy and out-of-gas vulnerabilities. △ Less

Submitted 22 November, 2019; v1 submitted 16 February, 2019; originally announced February 2019.