کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423444 685228 2007 22 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
State-oriented Noninterference for CCS
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
State-oriented Noninterference for CCS
چکیده انگلیسی

We address the question of typing noninterference (NI) in the calculus CCS, in such a way that Milner's translation into CCS of a standard parallel imperative language preserves both an existing NI property and the associated type system. Recently, Focardi, Rossi and Sabelfeld have shown that a variant of Milner's translation, restricted to the sequential fragment of the language, maps a time-sensitive NI property to that of Persistent Bisimulation-based Non Deducibility on Compositions (PBNDC) on CCS. However, since CCS was not equipped with a type system, the question of whether the translation preserves types could not be addressed. We extend Focardi, Rossi and Sabelfeld's result by showing that a slightly simpler variant of Milner's translation preserves a time-insensitive NI property on the full parallel language, by mapping it again to PBNDC. As a by-product, we formalise a folklore result, namely that Milner's translation preserves a behavioural equivalence on programs. We present a simple type system ensuring PBNDC on CCS, inspired by existing type systems for the π-calculus. Unfortunately, this type system as it stands is too restrictive to grant the expected type preservation result. We sketch a solution to overcome this problem.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 194, Issue 1, 8 November 2007, Pages 39-60