-
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.
-
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.
-
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.
-
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.
-
A multiagent based framework secured with layered SVM-based IDS for remote healthcare systems
Authors:
Mohammadreza Begli,
Farnaz Derakhshan
Abstract:
Since the number of elderly and patients who are in hospitals and healthcare centers are growing, providing efficient remote healthcare services seems very important. Currently, most such systems benefit from the distribution and autonomy features of multiagent systems and the structure of wireless sensor networks. On the one hand, securing the data of remote healthcare systems is one of the most…
▽ More
Since the number of elderly and patients who are in hospitals and healthcare centers are growing, providing efficient remote healthcare services seems very important. Currently, most such systems benefit from the distribution and autonomy features of multiagent systems and the structure of wireless sensor networks. On the one hand, securing the data of remote healthcare systems is one of the most significant concerns; particularly recent types of research about the security of remote healthcare systems keep them secure from eavesdropping and data modification. On the other hand, existing remote healthcare systems are still vulnerable against other common attacks of healthcare networks such as Denial of Service (DoS) and User to Root (U2R) attacks, because they are managed remotely and based on the Internet. Therefore, in this paper, we propose a secure framework for remote healthcare systems that consists of two phases. First, we design a healthcare system base on multiagent technology to collect data from a sensor network. Then, in the second phase, a layered architecture of intrusion detection systems that uses Support Vector Machine to learn the behavior of network traffic is applied. Based on our framework, we implement a secure remote healthcare system and evaluate this system against the frequent attacks of healthcare networks such as Smurf, Buffer overflow, Neptune, and Pod attacks. In the end, evaluation parameters of the layered architecture of intrusion detection systems prove the efficiency and correctness of our proposed framework.
△ Less
Submitted 13 April, 2021;
originally announced April 2021.
-
Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs
Authors:
Farzaneh Derakhshan,
Frank Pfenning
Abstract:
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes…
▽ More
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.
△ Less
Submitted 7 March, 2021; v1 submitted 14 January, 2020;
originally announced January 2020.
-
Circular Proofs as Session-Typed Processes: A Local Validity Condition
Authors:
Farzaneh Derakhshan,
Frank Pfenning
Abstract:
Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspo…
▽ More
Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspondence for a fragment of substructural logic with least and greatest fixed points. We describe the computational interpretation of the resulting infinitary proof system as session-typed processes, and provide an effectively decidable local criterion to recognize mutually recursive processes corresponding to valid circular proofs as introduced by Fortier and Santocanale. We show that our algorithm imposes a stricter requirement than Fortier and Santocanale's guard condition, but is local and compositional and therefore more suitable as the basis for a programming language.
△ Less
Submitted 9 May, 2022; v1 submitted 5 August, 2019;
originally announced August 2019.
