Cadre algébrique pour le renforcement de politique de sécurité sur des systèmes concurrents par réécriture automatique de programmes
|Authors:||Langar, Mohamed Mahjoub|
|Advisor:||Mejri, Mohamed; Adi, Kamel|
|Abstract:||One of the important goals of the software development process is proving that the produced systems always meet their requirements. However, establishing this goal is not only subtle and complex, but also requires high qualified persons. In addition, this operation is mostly omitted due to its high cost and the system is tested while trying to reduce the risk of errors as much as possible. The cost is, nevertheless, paid when this operation is required in order to avoid catastrophic consequences and major errors. In these cases, tools like theorem prover and those used for automatic generation of software are helpful to significantly reduce the cost of proof. Our aim is that this tool proves to be powerful and simple enough to generate benefits even to small companies and individuals with scarce budgets and limited theoretical skills . Many promising formal frameworks for automatic enforcement of security policies in programs have been proposed during the last years. Their goal is to ensure that a program respects a given security policy which generally specifies acceptable executions of the program and can be expressed in terms of access control problems, information flow, availability of resources, confidentiality, etc. The literature records various techniques for enforcing security policies belonging to mainly two principal classes: static approaches including typing theory, Proof Carrying Code, and dynamic approaches including reference monitors, Java stack inspection. Static analysis aims at enforcing properties before program execution. In dynamic analysis, however, the enforcement takes place at runtime by intercepting critical events during the program execution and halting the latter whenever an action is attempting to violate the property being enforced. Recently, several researchers have explored rewriting techniques in order to gather advantages of both static and dynamic methods. The idea consists in modifying a program statically, so that the produced version respects the requested requirements. The rewritten program is generated from the original one by adding, when necessary, some tests at some critical points to obtain the desired behaviors. This thesis aims to propose an algebraic and automatic approach that could generate from a given program, and a security policy, a new version of this program that respects the requested security policy. More precisely, we define an operator [symbol] that takes as input a process [symbol] and a security policy [symbol] and generates [symbol], a new process that respects the following conditions: [symbol] "satisfies" the security policy [symbol]. [symbol], behaviours of [symbol] are also behaviours of [symbol]. [symbol], all good behaviours of [symbol] are also behaviours [symbol]. The main results of our research are the following~: 1. The definition of a process algebra [symbol] offering an algebraic framework for the enforcement of security policies on concurrent systems. 2. The definition of a logic, denoted by [symbol], inspired from Kleene algebras and regular expressions. Basically, it allows to specify properties that can be checked on a trace-based model and properties related to infinite behavior (e.g. a server should not send the password of users). The choice of this logic is motivated by its syntax that is close to the one chosen for processes. In fact, this similarity is helpful to simplify the definition of our formal monitor. 3. The development of an optimization technique which, for a certain class of security properties, reduces the number of tests added in the target.|
|Document Type:||Thèse de doctorat|
|Open Access Date:||16 April 2018|
|Collection:||Thèses et mémoires|
All documents in CorpusUL are protected by Copyright Act of Canada.