In this project, we are investigating the general question of security in services/cloud computing where services are autonomous entities that co-exist within virtual groups called communities. The security is analysed from the perspectives of 1) trust that autonomous and selfish components can establish towards each other and 2) detection of malicious components and their attacks. We model the trust and its propagation using probabilistic systems where objective and subjective trust sources are considered. The main objective is to develop a collusion-resilient trust framework to deal with attacks aiming to mislead trust results and a trust-based coalitional game that enables autonomous entities to form distributed trustworthy systems. Game theoretical solutions and concepts are being used and proposed.

In this project, we investigate how we can best employ game theory to improve the security and efficiency of outsourced databases (cloud databases). Outsourced databases are stored on untrusted third-party servers (cloud database service provider) beyond the database owner control. Therefore, the database owner must employ data integrity assurance techniques to ensure the integrity of the outsourced database is not manipulated. Using the well-known data integrity assurance techniques such as encryption/decryption can be computationally costly process specially when applied to big data. The main objective of this project was to employ Stackelberg game theory to model the security game between a malicious database service provider and the database owner as a leader-follower security game. By solving the game, the database owner (being the leader in this game) finds the optimal mixed strategy as to what database table to verify at each verification moment. By committing to this optimal strategy, the database owner can ensure a higher payoff which translates to a higher probability of detecting any data manipulation.

In this project, we are interested in formalizing agent communication using formal logics and automatically verifying agent systems using the principal of model checking. Social commitments, knowledge and trust are the key concepts this project is analysing. The main idea is to verify the system against desirable properties derived from the requirements. The system is modeled as a mathematical structure capturing its behavior and transitions and the properties are expressed using formal and computational logical languages. Unlike traditional systems, intelligent systems exhibit autonomous and non-deterministic behaviors based on the dynamic knowledge of the autonomous agents forming the global system and their ability to commit to a complex course of actions. Verifying this type of systems is particularly challenging from the computational perspectives where new algorithms taking into consideration the autonomy and selfishness of agents must be defined and implemented.

Avionics systems are critical systems and their specification and verification are challenging issues. Ensuring safety in such systems is a high priority to prevent catastrophic events. The avionics industry has introduced a rigorous certification process described in the DO-178B standard that provides guidance for producing software of airborne systems that performs its function with a level of confidence in safety and complies with airworthiness requirements. In this project, we are investigating the modeling part of avionics components and their specification using formal methods. The main objective is to propose an operational and formal approach that addresses the issues of modeling, verifying, and testing avionics systems. Combining testing and formal verification in the same framework is one of the main gaols of this project.