Asynchronous and deterministic objects

We present in this article a precise security model for data confidentiality in the framework of asynchronous and deterministic objects. Our underlying programming model is based on active objects, asynchronous communications, and data-flow synchronizations. We extend its theoretical foundation, a calculus named ASP (Asynchronous Sequential Processes), with security levels attached to activities (active objects) and transmitted data. We design a security model in order to guarantee the property of data confidentiality within an application; this security model takes advantages of both mandatory and discretionary access models. Then, we extend the formal semantics of ASP with predicate conditions that provides a formal security framework. At the same time, it makes it possible to dynamically check for unauthorized information flows. As a final result, we formally prove that, all authorized communication paths are secure, which means that no disclosure of information can happen. This th...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Denis Caromel, Ludovic Henrio, Bernard P. Serpette
• Keywords: Calculus Named Asp, Discretionary Access Models, POPL 2004, Programming Languages, Security Model