A typed encoding of boxed into safe ambients

摘要

We present: (i) an encoding of Boxed Ambients into a variant of Safe Ambients; and (ii) a new type system for multi-level security of Safe Ambients in the style of Cardelli et al. (Information and Computation 177(2), 160-194 (2002)) and Dezani-Ciancaglini and Salvo (Security types for mobile safe ambients. In: Proceedings of ASIAN '00, LNCS 1961, pp. 215-236. Springer Verlag (2000)). Then, we show that the types, when applied to the encoded BA proceses, permits to accurately verify Mandatory Access Control policies of the source processes.