scholarly journals Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)

10.29007/t2h1 ◽  
2018 ◽  
Author(s):  
Klaus von Gleissenthall ◽  
Andrey Rybalchenko ◽  
Santiago Zanella-Béguelin
Keyword(s):  
Automatic Generation ◽  
Tool Support ◽  
Relational Properties ◽  
Security Properties ◽  
Probabilistic Programs

Some security properties go beyond what is expressible in terms of anindividual execution of a single program. In particular, many securitypolicies in cryptography can be naturally phrased as relationalproperties of two open probabilistic programs. Writing and verifyingproofs of such properties is an error-prone task that calls forautomation and tool support. One of the main difficulties inautomating these proofs lies in finding adequate relational invariantsfor loops and specifications for program holes.In this talk we showhow to automate proofs of relational properties of open probabilisticprograms by adapting techniques for the automatic generation ofuniversally quantified invariants in a non-relational setting.

scholarly journals Security assurance cases—state of the art of an emerging approach

2021 ◽  
Vol 26 (4) ◽  
Author(s):  
Mazen Mohamad ◽  
Jan-Philipp Steghöfer ◽  
Riccardo Scandariato
Keyword(s):  
State Of The Art ◽  
Tool Support ◽  
Security Assurance ◽  
The Past ◽  
Depth Analysis ◽  
Structured Argumentation ◽  
Security Properties ◽  
Standards And Regulations ◽  
Assurance Cases ◽  
Security Standards

AbstractSecurity Assurance Cases (SAC) are a form of structured argumentation used to reason about the security properties of a system. After the successful adoption of assurance cases for safety, SAC are getting significant traction in recent years, especially in safety-critical industries (e.g., automotive), where there is an increasing pressure to be compliant with several security standards and regulations. Accordingly, research in the field of SAC has flourished in the past decade, with different approaches being investigated. In an effort to systematize this active field of research, we conducted a systematic literature review (SLR) of the existing academic studies on SAC. Our review resulted in an in-depth analysis and comparison of 51 papers. Our results indicate that, while there are numerous papers discussing the importance of SAC and their usage scenarios, the literature is still immature with respect to concrete support for practitioners on how to build and maintain a SAC. More importantly, even though some methodologies are available, their validation and tool support is still lacking.

scholarly journals Proving uniformity and independence by self-composition and coupling

10.29007/vz48 ◽  
2018 ◽  
Author(s):  
Gilles Barthe ◽  
Thomas Espitau ◽  
Benjamin Grégoire ◽  
Justin Hsu ◽  
Pierre-Yves Strub
Keyword(s):  
Differential Privacy ◽  
Proof Assistant ◽  
Proof Technique ◽  
Formal Reasoning ◽  
Program Logic ◽  
Relational Properties ◽  
Probabilistic Couplings ◽  
Probabilistic Processes ◽  
Probabilistic Programs ◽  
Classical Proof

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL—whose proofs are formal versions of proofs by coupling—can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.

A Tool Support for Secure Software Integration

2012 ◽  
pp. 248-268
Author(s):  
Khaled M. Khan ◽  
Jun Han
Keyword(s):  
Security Requirements ◽  
Tool Support ◽  
Software Integration ◽  
Research Outcomes ◽  
Secure Software ◽  
Security Properties ◽  
Automatic Tool ◽  
Software Services

This paper presents a tool for the integration of security-aware services based applications that is constructed on the principles of security characterization of individual software services. The tool uses the technique of reasoning between the ensured security properties of the services and the security requirements of the user’s system. Rather than reporting the research outcomes, in this paper the authors describe the architecture and capabilities of the tool for secure software integration. The main objective of this paper is to show that an automatic tool support could assist the process of security-aware service based software integration.

A Tool Support for Secure Software Integration

2010 ◽  
Vol 1 (2) ◽  
pp. 35-56
Author(s):  
Khaled Md Khan ◽  
Jun Han
Keyword(s):  
Security Requirements ◽  
Tool Support ◽  
Software Integration ◽  
Research Outcomes ◽  
Secure Software ◽  
Security Properties ◽  
Automatic Tool ◽  
Software Services

This paper presents a tool for the integration of security-aware services based applications that is constructed on the principles of security characterization of individual software services. The tool uses the technique of reasoning between the ensured security properties of the services and the security requirements of the user’s system. Rather than reporting the research outcomes, in this paper the authors describe the architecture and capabilities of the tool for secure software integration. The main objective of this paper is to show that an automatic tool support could assist the process of security-aware service based software integration.

The Role of Visual Distractors in the Simon Effect

2017 ◽  
Vol 64 (6) ◽  
pp. 387-397 ◽  
Author(s):  
Luisa Lugli ◽  
Stefania D’Ascenzo ◽  
Roberto Nicoletti ◽  
Carlo Umiltà
Keyword(s):  
Simon Effect ◽  
Simon Task ◽  
Automatic Generation ◽  
Spatial Code ◽  
Attentional Model ◽  
Previous Evidence ◽  
Spatial Stimulus ◽  
Attentional Resources ◽  
Code Changes

Abstract. The Simon effect lies on the automatic generation of a stimulus spatial code, which, however, is not relevant for performing the task. Results typically show faster performance when stimulus and response locations correspond, rather than when they do not. Considering reaction time distributions, two types of Simon effect have been individuated, which are thought to depend on different mechanisms: visuomotor activation versus cognitive translation of spatial codes. The present study aimed to investigate whether the presence of a distractor, which affects the allocation of attentional resources and, thus, the time needed to generate the spatial code, changes the nature of the Simon effect. In four experiments, we manipulated the presence and the characteristics of the distractor. Findings extend previous evidence regarding the distinction between visuomotor activation and cognitive translation of spatial stimulus codes in a Simon task. They are discussed with reference to the attentional model of the Simon effect.

Sign in / Sign up

Export Citation Format

Share Document