Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model

2010 ◽  
Vol 9 (8) ◽  
pp. 1521-1556 ◽  
Author(s):  
Bo Meng ◽  
Wei Huang ◽  
Jun Qin
Keyword(s):  
Automatic Verification ◽  
Symbolic Model ◽  
Internet Voting ◽  
Security Properties

scholarly journals Compositional and Symbolic Model-Checking of Real-Time Systems

1996 ◽  
Vol 3 (59) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Automatic Verification ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Verification Tools ◽  
State Region ◽  
Time Systems

Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.

scholarly journals Multi-Level Policy Model Access Control Security Operating Systems of the Windows Family

2021 ◽  
pp. 41-56
Author(s):  
Vasilii Kozachok ◽  
◽  
Alexander Kozachok ◽  
Evgenii Kochetkov ◽  
◽  
...  
Keyword(s):  
Access Control ◽  
Operating Systems ◽  
Security Policy ◽  
Information Leakage ◽  
Automatic Verification ◽  
Software Environment ◽  
Policy Model ◽  
Windows Nt ◽  
Mandatory Access Control ◽  
Security Properties

The purpose of research – development of a more advanced Windows NT family access control mechanism to protect against information leakage from memory by hidden channels. The method of research – analysis of Windows NT family models of mandatory access control and integrity control, modeling of access control security policy for specified security properties, automatic verification of models. The Lamport Temporal Logic of Actions (TLA +) used to describe the model and its specification is used. TLA+ allows automatic verification of the model with the specified security properties. The result of research – revealed the main limitations of the existing mandatory integrity control of operating systems of the Windows NT family. A set of structures of a multilevel model has been developed, reflecting the attributes that are significant for modeling the process of access of subjects to objects. The key mechanisms of access control in the operating system are modeled: management of users, groups, subjects, objects, roles, rights, discretionary and mandatory access control, mandatory integrity control - multilevel control of subjects’ access to objects. The model defines a mechanism for controlling the creation of subjects based on executable files to organize an isolated software environment. The values of the attributes of the model variables for the initialization stage are determined. The invariants of variables correctness in the process of verification and subjects to objects safe access are developed. The model was specified using the TLA + modeling language and verified.

Sign in / Sign up

Export Citation Format

Share Document