The use of security patterns has been recognized as effective in mitigating vulnerabilities in software systems. However, it is still not well understood how they can be applied systematically and effectively in concrete systems to achieve the best results. We present a formal approach based on the Alloy model checker to detect information disclosure vulnerabilities and enforce appropriate security patterns automatically. The approach helps improve the overall security posture of software systems while reducing the dependence on manual security analysis. We demonstrate the usability of our approach through the use case of a Smart Meter Gateway. The proposed approach is generic and constitutes a significant advancement toward systematic methods for designing secure software systems.

Legal contracts specify requirements for business transactions. As any other requirements specification, contracts may contain errors and violate properties expected by contracting parties. Symboleo was recently proposed as a formal specification language for legal contracts. This paper presents SymboleoPC, a tool for analyzing Symboleo contracts using model checking. It highlights the architecture, implementation and testing of the tool, as well as a scalability evaluation with respect to the size of contracts and properties to be checked through a series of experiments. The results suggest that SymboleoPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.

Smart contracts (SCs) are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are popular choices for SC development. However, there is a gap in the knowledge of SCs between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. In this paper, we propose a tool-supported method for translating Symboleo specifications into smart contracts. We have extended the current Symboleo IDE, implemented the ontology and semantics of Symboleo into a reusable library, and developed the Symboleo2SC tool to generate Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. The results shows that legal contract specifications in Symboleo can be fully converted to SCs for monitoring purposes. Moreover, Symboleo2SC helps simplify the SC development process, saves development effort, and helps reduce risks of coding errors.

Legal contracts specify the terms and conditions (in essence, requirements) that apply to business transactions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. This paper proposes a formal specification language for contracts, called Symboleo, where contracts consist of collections of obligations and powers that define the legal contract's compliant executions. The formal semantics of Symboleo is based on an extension of an ontology for Law and is described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations and powers. Our proposal includes a preliminary evaluation through the specification of a real life-inspired Sale-of-Goods contract, with a prototype execution engine. We envision this language to enable formally verifying contracts to detect requirements-level issues and to generate executable smart contracts (e.g., on blockchain technology).

The visual aspect of metamodelling languages is an efficient lever to overcome the complexity of specifying systems. In many application domains, these systems are generally characterized by the sensitivity and criticality of their contents and formalism is yet an essential desired goal. This paper considers the domain of access control specification languages and proposes a metamodelling paradigm with capabilities for specifying both semantics and structuring elements. The paradigm is applicable to a wide range of systems, especially decision systems. We describe how to specify semantics of domain specific systems at the metamodel and model levels. The paradigm defines reusable rules allowing mapping the models, including their semantics, to first order logic programs. It represents a methodical approach to elaborate domain specific languages endowed with visual aspects and means of reasoning on formal specifications.

Many models, methods, techniques, and systems have been developed to preserve the integrity of data and guarantee an acceptable level of security over networks. Protection from illegitimate data access and control of information flow are two main goals. This paper presents new techniques that address two main issues: information protection at various levels of granularity and data flow control We first investigate challenges and limits of established access control models regarding flow control. We then introduce a new flow control model based on granularity, the GBFC. GBFC is capable of guaranteeing flow control under reasonable assumptions. In addition, it offers advantages such as adaptability, full control, reliability and compatibility amongst others. Essentially, in GBFC classified information at suitable levels of granularity is accessible through references and information flow control is applied on the references. We also introduce the concepts of views for information access and Noise Injection that represent building blocks for the Granularity Based Flow Control. With noise injection, a document can be transformed into different views to erase or replace protected information and this transformation can be made almost undetectable to the unauthorized reader. Therefore, inference can be made much more difficult with this method. The GBFC model is intended to complement, rather than replace, existing access control methods.

In Cloud environments, Cloud users have the possibility to put their sensitive data on Cloud servers, which opens the door to security challenges concerning data protection. In this context, access control is of vital importance, since it provides security mechanisms to protect against inappropriate access to data. Unfortunately, classical access control models such as DAC, MAC, RBAC or ABAC are not sufficiently expressive for highly flexible and dynamic environments such as those found in the Cloud. Often, a combination of elements of these models is necessary in order to properly express varied data protection needs. In this paper, we present a new approach called CatBAC (Category Based Access Control), for building dedicated access control models starting from an abstract meta-model. Hence, in our approach, a meta-model can be refined in accordance with the high level security policies of each specific user. Our framework for building access control models can be implemented as a Cloud service and Cloud providers will then apply different concrete access control models produced by each user to process its incoming access requests.

Several formal access control models are known in the literature, such as DAC, MAC, RBAC, etc. However, these models cannot meet new security requirements required by flexible and dynamic environments which necessitate a combination of elements of these models, in order to properly express varied data protection needs. In this paper, we present a new method for the specification of access control systems. The method makes it possible to design an access control system specific to the high level policy of an organization. The method is based on a generic UML meta-model of access control called CatBAC (Category Based Access Control), together with a refinement process for the extraction of security requirements from high level policies. Based on the category concept, the CatBAC meta-model allows specifying hybrid policies of access control.

Many access control models have been proposed in the literature, and they have been extensively studied under the acronyms of DAC, MAC, RBAC, ABAC, etc. Each of these models has been studied in isolation, but some real-life situations need elements of several of them, in order to properly express data protection needs of complex organizations. A formal framework is presented, that allows not only to combine elements of these models, but also to generalize them in new ways. This framework includes elements of a lifecycle methodology, which starts with a UML-based formalism, called UACML, that expresses semantic elements (classes and their relationships) needed for general access control systems. It continues with the representation of UACML diagrams in our language CatBAC. The latter is a compact textual representation of UACML that makes it possible to express realistic policy systems involving many entities and many constraints. CatBAC is based on Prolog, and this makes it possible to implement analysis and verification tools.

Web sites usually express their privacy practices in natural language text that is often complex, informal and possibly confusing. The platform for Privacy Preference (P3P) has been proposed by W3C as a technology for expressing privacy practices of web sites in precise, machine readable language. This paper provides an account of the current status of research on P3P and proposes directions for future research, together with some possible solutions. Cloud computing (SaaS), anti-phishing, and mobile applications are some of the aspects that we consider. We claim that P3P and P3P-based techniques have considerable potential to be developed beyond their current status. The challenge is to design formalized privacy policy languages that can enable computers to process the privacy practices of web sites. In this way, many privacy issues, such as filtering web sites, combining their policies, etc., will be able to be dealt with automatically by privacy agents.

Traditional security and access control systems, such as MLS/Bell-LaPadula, RBAC are rigid and do not contain automatic mechanisms through which a system can increase or decrease users' access to classified information. Therefore, in this paper, we propose a risk-based decision method for an access control system. Firstly, we dynamically calculate the trust and risk values for each subject-object pair. Both values are adaptive, reflecting the past behavior of the users with particular objects. The past behavior is evaluated based on the history of reward and penalty points. These are assigned by the system after the completion of every transaction. Secondly, based on the trust and risk values, an access decision is made.

In enterprise environments, the task of assigning access control rights to subjects for resources is not trivial. Because of their complexity, distribution and size, access control policies can contain anomalies such as inconsistencies, which can result in security vulnerabilities. A set of access control policies is inconsistent when, for specific situations different incompatible policies can apply. Many researchers have tried to address the problem of inconsistency using methods based on formal logic. However, this approach is difficult to implement and inefficient for large policy sets. Therefore, in this paper, we propose a simple, efficient and practical solution for detecting inconsistencies in access control policies with the help of a modified C4.5 data classification algorithm.

Commonly known access control systems respond to users' requests to perform actions on protected objects by giving binary answers such as permit or deny. The decisions are taken on the basis of access control policies, where the risk of allowing access is not necessarily taken into explicit consideration. In this paper, we introduce RBACRmodel (Role Based Access Control Model with Risk), in which each access control decision is taken after consideration of risk assessment. The proposed risk assessment method considers partial orderings on objects and actions to capture the notions of importance of objects and criticality of actions, and determines the risk of assigning a specific role to a specific user. The case of role delegation is also considered.

Functional scenarios describing system views, uses, or services are a common way of capturing requirements of distributed systems. However, integrating individual scenarios in different ways may result in different kinds of unexpected or undesirable interactions. We present an innovative approach based on the combined use of two notations. The first one is a recent visual notation for causal scenarios called use case maps (UCMs), which is used to capture and integrate the requirements. Integrating UCMs together helps avoiding many interactions before any prototype is generated. The second notation is the formal specification language LOTOS. UCM scenarios are translated into high-level LOTOS specifications, which can be used to validate the requirements formally through numerous techniques, including functional testing based on UCMs. LOTOS possesses powerful testing concepts and tools that we use for the detection of remaining undesirable interactions. To illustrate these concepts, we use a simple connection example and results from the capture and the validation of several telephony features from the First Feature Interaction Contest.

Abstract LOTOS is an executable specification language for distributed systems currently being standardized within ISO as a tool for the formal specification of open systems interconnection protocols and services. It is based on an extended version of Milner's calculus of communicating systems (CCS) and on ACT ONE abstract data type (ADT) formalism. A brief introduction to LOTOS is given, along with a discussion of LOTOS operational semantics, and of the executability of LOTOS specifications. Further, an account of a prototype LOTOS interpreter is given, which includes an interactive system that allows the user to direct the execution of a specification (for example, for testing purposes). The interpreter was implemented in YACC/LEX, C and Prolog. The following topics are discussed: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of ADT value expressions and extended CCS behaviour expressions. It is shown that the interpreter can be used in a variety of ways: to recognize whether a given sequence of interactions is allowed by the specification; to generate randomly chosen sequences of interactions; in a user‐guided generation mode, etc.

LOTOS is an executable specification language for protocols and services currently being standardized within ISO. It is based on an extended version of Milner's Calculus of Communicating Systems (CCS) and ACT ONE Abstract Data Type formalism. After a brief introduction to LOTOS, we give here an account of a prototype LOTOS interpreter, which includes an interactive system that allows the user to direct the execution of a specification. The interpreter was implemented in YACC/LEX, C, and Prolog. The discussion includes the following topics: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of Abstract Data Type value expressions and CCS* clauses.

A language for defining sequential file structures, characterized as nested sequences of records having in common certain keys and types, is presented. "Input schemata" are defined as program skeletons that contain all the necessary control structure to process a specified file. A method for obtaining an input schema from the corresponding file structure definition is given. The method is based on attributed grammars, and has been implemented in the programming language PROLOG. This constitutes a formalization of some aspects of the data-directed program design method of Jackson and Warnier. Examples of applications of this method to business data processing problems such as file updating and report generation are given.

Concepts such as "max,mal parallehsm," "greater parallelism," and "instruction look-ahead" are mvesugated m the framework of program schemata theory A method for increasing the parallelism of a program schema by changmg its control structure and the name of Jts variables Js given.A characterization result of maximal parallehsm, a method for approxunating the maximally parallel form of a given finite schema, and a space-tune tradeoff pnnctple are obtained It ts shown that maximal paraUehsm is a decidable property for fimte schemata, but that there are fmite schemata whose maximally parallel form requires an infinite control and an mfmtte number of memory variables

The effects of changing the names of the variables in program schemata are studied.Two schemata are said to be "strongly slmdar" if they compute the same values (intermediate values as well as final ones) in the same order A method for performing renammgs in such a way that the resulting schema is strongly similar to the original one is given Also, there exists a class of schemata such that any two schemata in the class for which one is not obtained from the other by the method above are not strongly similar These results are then apphed to the problem of memory economy, ~ e the problem of reducing the number of .variables in a schema.Previously known results showing that one version of this problem is equivalent to the well-known "graph coloring problem" of graph theory are presented, together with a new solution involving "state sphning" in the schema Finally, it is shown that in some cases It is decidable whether two schemata are strongly simdar.