Email Gateway (Aug 22 2022 at 13:35): Email Gateway (Aug 22 2022 at 13:35):From: Lawrence Paulson <lp15@cam.ac.uk>
Pasquale Noce continues his work on noninterference in CSP, this time considering concurrent composition. More details below. Many thanks, Pasquale!
Larry Paulson
In his outstanding work on Communicating Sequential Processes, Hoare has defined two fundamental binary operations allowing to compose the input processes into another, typically more complex, process: sequential composition and concurrent composition. Particularly, the output of the latter operation is a process in which any event not shared by both operands can occur whenever the operand that admits the event can engage in it, whereas any event shared by both operands can occur just in case both can engage in it.
This paper formalizes Hoare's definition of concurrent composition and proves, in the general case of a possibly intransitive policy, that CSP noninterference security is conserved under this operation. This result, along with the previous analogous one concerning sequential composition, enables the construction of more and more complex processes enforcing noninterference security by composing, sequentially or concurrently, simpler secure processes, whose security can in turn be proven using either the definition of security, or unwinding theorems.
http://www.isa-afp.org/entries/Noninterference_Concurrent_Composition.shtml
Last updated: Apr 16 2024 at 20:15 UTC