1. 21
  1.  

  2. 2

    Great intuitive walk through a real protocol and TLA, thanks!

    Did anyone else really want there to be a Confidentiality to go with the Integrity and Availability?

    1. 2

      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.

      1. 1

        I was primarily being facetious, thanks for spinning it into something useful and interesting! I’ll take a look. Much appreciated.

        1. 2

          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.