That property is non-interference. It will be a product’s formal, security policy. It’s used in separation kernels like seL4 and INTEGRITY-178B. A high[er]-security attempt at Xen that probably did a covert, channel analysis or had non-interference policy was Xenon (pdf slides). Note that was first link I found on mobile: didnt read it in full.
Oh ok haha. The good news is that, while failing to find a non-interference example in TLA+, I did find some submission-worthy stuff in mix of free and paywalled sources. Ill submit them next week.
Great intuitive walk through a real protocol and TLA, thanks!
Did anyone else really want there to be a
Confidentialityto go with theIntegrityandAvailability?That property is non-interference. It will be a product’s formal, security policy. It’s used in separation kernels like seL4 and INTEGRITY-178B. A high[er]-security attempt at Xen that probably did a covert, channel analysis or had non-interference policy was Xenon (pdf slides). Note that was first link I found on mobile: didnt read it in full.
I was primarily being facetious, thanks for spinning it into something useful and interesting! I’ll take a look. Much appreciated.
Oh ok haha. The good news is that, while failing to find a non-interference example in TLA+, I did find some submission-worthy stuff in mix of free and paywalled sources. Ill submit them next week.