Secure information sharing in social agent interactions using information flow analysis

Both static (design-time) and dynamic (run-time) security type checking are employed to guarantee no information leakage can occur in annotated agent interaction models. The proposed security type system is discussed and then formally evaluated by proving its properties. Two disadvantages of the pure dynamic analysis are its late detection and its inability to detect implicit information flows. We overcome these issues by performing static analysis. The proposed security type system supports non-interference, i.e. high-security input to the program never affect low-security output. However, it disregards information leaks due to the termination of the program.