Combining behavioural types with security analysis

DOI10.1016/J.JLAMP.2015.09.003zbMATH Open1330.68045DBLPjournals/jlp/BartolettiCDDGP15arXiv1510.02229OpenAlexW3105067267WikidataQ57652373 ScholiaQ57652373MaRDI QIDQ890614FDOQ890614

Authors: Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jorge A. Pérez, Peter J. Thiemann, Bernardo Toninho, Hugo Torres Vieira, Jovanka Pantović 

Publication date: 10 November 2015

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1510.02229

Recommendations

• Preface to special issue: Behavioural types
• Preface to special issue: Behavioural types
• A gentle introduction to multiparty asynchronous session types
• scientific article; zbMATH DE number 7075898
• Relating Process Languages for Security and Communication Correctness (Extended Abstract)

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• The Orc Programming Language
• Secure distributed programming with value-dependent types
• Title not available (Why is that?)
• A framework for defining logics
• Linear logic
• Multiparty session types meet communicating automata
• On the realizability of contracts in dishonest systems
• Modelling and verifying contract-oriented systems in Maude
• Multiparty asynchronous session types
• Contract-oriented computing in CO\(_2\)
• A theory of agreements and protection
• Verifying persistent security properties
• Subtyping for session types in the pi calculus
• Types for role-based access control of dynamic web data
• Secure Enforcement for Global Process Specifications
• Regulating Data Exchange in Service Oriented Applications
• Session types for access and information flow control
• Typing access control and secure information flow in sessions
• Correspondence assertions for process synchronization in concurrent communications
• Type-based information flow analysis for the \(\pi\)-calculus
• Global Progress in Dynamically Interleaved Multiparty Sessions
• A theory of design-by-contract for distributed multiparty interactions
• Session types as intuitionistic linear propositions
• Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines
• A type system for lock-free processes
• Title not available (Why is that?)
• Proof-carrying code in a session-typed process calculus
• Linear logical relations and observational equivalences for session-based concurrency
• Certification of programs for secure information flow
• Dynamic typing: Syntax and proof theory
• Objects and session types
• Deadlock and lock freedom in the linear \(\pi\)-calculus
• Type checking a multithreaded functional language with session types
• Foundations of security analysis and design. Tutorial lectures
• Modelling dynamic web data
• Typing correspondence assertions for communication protocols
• Typing the behavior of software components using session types
• The security pi-calculus and non-interference
• Session Types with Gradual Typing
• Stateful contracts for affine types
• Security Types for Dynamic Web Data
• Linearly refined session types
• Trustworthy Global Computing
• Gradual Typing for Annotated Type Systems
• Security types for dynamic web data

Cited In (8)

• Relating Process Languages for Security and Communication Correctness (Extended Abstract)
• Dynamic role authorization in multiparty conversations
• Self-adaptation and secure information flow in multiparty communications
• A gentle introduction to multiparty asynchronous session types
• Verifiable abstractions for contract-oriented systems
• Preface to special issue: Behavioural types
• Preface to special issue: Behavioural types
• Discretionary Information Flow Control for Interaction-Oriented Specifications

Uses Software

• SPARK
• Maude
• COWS
• Orc
• Flow Caml
• Jif
• Scribble
• F*
• JSFlow

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)