Combining behavioural types with security analysis
From MaRDI portal
Abstract: Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.
Recommendations
Cites work
- scientific article; zbMATH DE number 4018370 (Why is no real title available?)
- scientific article; zbMATH DE number 1538026 (Why is no real title available?)
- A framework for defining logics
- A theory of agreements and protection
- A theory of design-by-contract for distributed multiparty interactions
- A type system for lock-free processes
- Certification of programs for secure information flow
- Contract-oriented computing in CO\(_2\)
- Correspondence assertions for process synchronization in concurrent communications
- Deadlock and lock freedom in the linear \(\pi\)-calculus
- Dynamic typing: Syntax and proof theory
- Foundations of security analysis and design. Tutorial lectures
- Global Progress in Dynamically Interleaved Multiparty Sessions
- Gradual Typing for Annotated Type Systems
- Linear logic
- Linear logical relations and observational equivalences for session-based concurrency
- Linearly refined session types
- Modelling and verifying contract-oriented systems in Maude
- Modelling dynamic web data
- Multiparty asynchronous session types
- Multiparty session types meet communicating automata
- Objects and session types
- On the realizability of contracts in dishonest systems
- Proof-carrying code in a session-typed process calculus
- Regulating Data Exchange in Service Oriented Applications
- Secure Enforcement for Global Process Specifications
- Secure distributed programming with value-dependent types
- Security Types for Dynamic Web Data
- Security types for dynamic web data
- Session Types with Gradual Typing
- Session types as intuitionistic linear propositions
- Session types for access and information flow control
- Stateful contracts for affine types
- Subtyping for session types in the pi calculus
- The Orc Programming Language
- The security pi-calculus and non-interference
- Trustworthy Global Computing
- Type checking a multithreaded functional language with session types
- Type-based information flow analysis for the \(\pi\)-calculus
- Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines
- Types for role-based access control of dynamic web data
- Typing access control and secure information flow in sessions
- Typing correspondence assertions for communication protocols
- Typing the behavior of software components using session types
- Verifying persistent security properties
Cited in
(8)- Discretionary Information Flow Control for Interaction-Oriented Specifications
- Verifiable abstractions for contract-oriented systems
- Preface to special issue: Behavioural types
- Preface to special issue: Behavioural types
- Dynamic role authorization in multiparty conversations
- Self-adaptation and secure information flow in multiparty communications
- A gentle introduction to multiparty asynchronous session types
- Relating Process Languages for Security and Communication Correctness (Extended Abstract)
This page was built for publication: Combining behavioural types with security analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q890614)
