1. 23
    1. 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.

Stories with similar links:

  1. Using TLA+ to understand Xen vchan via raymii 4 years ago | 13 points | no comments