Quantitative information flow is a rigorous approach for evaluating the security of a system. It is used to quantify the amount of secret information leaked to the public outputs. In this paper, we propose an automated approach for quantitative information flow analysis of concurrent programs. Markovian processes are used to model the behavior of these programs. To this end, we assume that the attacker is capable of observing the internal behavior of the program and propose an equivalence relation, back-bisimulation, to capture the attacker's view of the program behavior. A partition refinement algorithm is developed to construct the back-bisimulation quotient of the program model and then a quantification method is proposed for computing the information leakage using the quotient. Finally, an anonymous protocol, dining cryptographers, is analyzed as a case study to show applicability and scalability of the proposed approach.

Information leakage is the flow of information from secret inputs of a program to its public outputs. One effective approach to identify information leakage and potentially preserve the confidentiality of a program is to quantify the flow of information that is associated with the execution of that program, and check whether this value meets predefined thresholds. For example, the program may be considered insecure, if this quantified value is higher than the threshold. In this paper, an automated method is proposed to compute the information leakage of probabilistic programs. We use Markov chains to model these programs, and reduce the problem of measuring the information leakage to the problem of computing the joint probabilities of secrets and public outputs. The proposed method traverses the Markov chain to find the secret inputs and the public outputs and subsequently, calculate the joint probabilities. The method has been implemented into a tool called PRISM-Leak, which uses the PRISM model checker to build the Markov chain of input programs. The applicability of the proposed method is highlighted by analyzing a probabilistic protocol and quantifying its leakage.

Secure information flow checks whether sensitive information leak to public outputs of a program or not. It has been widely used to analyze the security of various programs and protocols and guarantee their confidentiality and robustness. In this paper, the problem of verifying secure information flow of concurrent probabilistic programs is discussed. Programs are modeled by Markovian processes and secure information flow is specified by observational determinism. Then, two algorithms are proposed to verify observational determinism in the Markovian model. The algorithms employ a trace-based approach to traverse the model and check for satisfiability of observational determinism. The proposed algorithms have been implemented into a tool called PRISM-Leak, which is constructed on the PRISM model checker. An anonymity protocol, the dining cryptographers, is discussed as a case study to show how PRISM-Leak can be used to evaluate the security of programs. The scalability of the tool is demonstrated by comparing it to the state-of-the-art information flow tools.

Quantitative information flow is an important technique for measuring information leakage of a program. It is widely used in analyzing anonymity protocols and timing channels. One area of interest is to quantify the information leakage of multi-threaded programs, which has not been well-studied in prior work. In this paper, an automated trace-based approach is proposed to precisely quantify information leakage of shared-memory multi-threaded programs. The approach takes into account the effect of schedulers and leakage in intermediate states of executions. The programs are modeled by Markovian processes. Then, variants of information leakage, including expected, bounded time, maximum, and minimum leakages are measured. The validity of the approach is demonstrated by implementing it in a tool PRISM-Leak, which is built upon PRISM, a probabilistic model checker. Finally, two case studies are utilized to analyze and compare the approach against state-of-the-art leakage quantification tools.

Keywords: Quantitative information flow, Information leakage, Multi-threaded program, Markovian processes, Confidentiality, PRISM-Leak

Preserving the confidentiality of information is a growing concern in software development. Secure information flow is intended to maintain the confidentiality of sensitive information by preventing them from flowing to attackers. This paper discusses how to ensure confidentiality for multi-threaded programs through a property called observational determinism. Operational semantics of multi-threaded programs are modeled using Kripke structures. Observational determinism is formalized in terms of divergence weak low-bisimulation. Bisimulation is an equivalence relation associating executions that simulate each other. The new property is called bisimulation-based observational determinism. Furthermore, a model checking method is proposed to verify the new property and ensure that secure information flow holds in a multi-threaded program. The model checking method successively refines the Kripke model of the program until the quotient of the model with respect to divergence weak low-bisimulation is reached. Then, bisimulation-based observational determinism is checked on the quotient, which is a minimized model of the concrete Kripke model. The time complexity of the proposed method is polynomial in the size of the Kripke model. The proposed approach has been implemented on top of PRISM, a probabilistic model checking tool. Finally, a case study is discussed to show the applicability of the proposed approach.

Weak probabilistic noninterference is a security property for enforcing confidentiality in multi-threaded programs. It aims to guarantee secure flow of information in the program and ensure that sensitive information does not leak to attackers. In this paper, the problem of verifying weak probabilistic noninterference by leveraging formal methods, in particular algorithmic verification, is discussed. Behavior of multi-threaded programs is modeled using probabilistic Kripke structures and formalize weak probabilistic noninterference in terms of these structures. Then, a verification algorithm is proposed to check weak probabilistic noninterference. The algorithm uses an abstraction technique to compute quotient space of the program with respect to an equivalence relation called weak probabilistic bisimulation and does a simple check to decide whether the security property is satisfied or not. The progress made is demonstrated by a real-world case study. It is expected that the proposed approach constitutes a significant step towards more widely applicable secure information flow analysis.

This paper proposes an approach to verify information flow security of concurrent programs. It discusses a hyperproperty called observational determinism which aims to ensure secure information flow in concurrent programs, and proves how this hyperproperty can be verified by stutter equivalence checking. More precisely, it defines observational determinism in terms of stutter equivalence of all traces having the same low initial value and shows how stutter trace equivalence can be verified by computing a divergence stutter bisimulation quotient. The approach is illustrated by verifying a small example.

Hill Cipher (HC) is a matrix-based polygraph symmetric data encryption method. In 2011, Desoky et al. proposed the Bitwise Hill Crypto System (BHC) which is based on bit arithmetic. In this paper, we analyze BHC and show that it is insecure. Then, we propose a new modification using chaotic maps which provides better security.

Hill Cipher (HC) is a matrix-based polygraph symmetric data encryption method. In 2011, Desoky et al. proposed the Bitwise Hill Crypto System (BHC) which is based on bit arithmetic. In this paper, we analyze BHC and show that it is insecure. Then, we propose a new modification using chaotic maps which provides better security.

In the real-world, there are many types of software systems and software engineers always deal with changes. The value of large systems decreases significantly as the requirements and operational environment change over time. Modern software systems are expected to have dynamic reconfigurations to cope with failure and changes. Software adaptation techniques try to overcome the change problem by reconfiguration. In this study, at first, the authors present a formal framework to represent the whole system and then, build a mathematical model called ‘adaptor’ based on adaptation contract and system architecture. The adaptor is used to define automatic fit between two different components of the system. Finally, for specifying the whole adaptor system the authors will introduce adaptor network using synchronisation vectors.

Keywords: adaptive systems;formal specification;software architecture;synchronisation;vectors;synchronisation vectors; adaptor system;mathematical model;system architecture;adaptation contract;change reconfiguration;change problem; software adaptation techniques;software systems;adaptive systems;dynamic reconfiguration specification;formal framework

Search engine is one of the most important tools for managing the massive amount of distributed web content. Web spamming tries to deceive search engines to rank some pages higher than they deserve. Many methods have been proposed to combat web spamming and to detect spam pages. One basic one is using classification, i.e., learning a classification model for classifying web pages to spam or non-spam. This work tries to select the best feature set for classification of web spam using imperialist competitive algorithm and genetic algorithm. Imperialist competitive algorithm is a novel optimization algorithm that is inspired by socio-political process of imperialism in the real world. Experiments are carried out on WEBSPAM-UK2007 data set, which show feature selection improves classification accuracy, and imperialist competitive algorithm outperforms GA.

Web spamming tries to deceive search engines to rank some pages higher than they deserve. Many methods have been proposed to combat web spamming and to detect spam pages. One basic method is using classification, i.e., learning a classification model from previously labeled training data and using this model for classifying web pages to spam or non-spam. A drawback of this method is that manually labeling a large number of web pages to generate the training data can be biased, non-accurate, labor intensive and time consuming. In this paper, we are going to propose a new method to resolve this drawback by using semi-supervised learning to automatically label the training data. To do this, we incorporate Expectation-Maximization algorithm that is an efficient and an important algorithm of semi-supervised learning. Experiments are carried out on the real web spam data, which show the new method, performs very well in practice.