Linux Mint drops Ubuntu Snap packages

Posted Jul 10, 2020 23:17 UTC (Fri) by ras (subscriber, #33059)
In reply to: Linux Mint drops Ubuntu Snap packages by stephen.pollei
Parent article: Linux Mint drops Ubuntu Snap packages

David Wheeler's paper is one solution, but I've never heard of an instance of the technique he describes catching anything.

On the other hand, the techniques Open Source has developed over the years has caught a few attempts to slip nefarious code in. Those techniques are:

1. A cryptographically sealed audit trail of every change (eg, git's sha1 sums).

2. Digitally signed commits, so if someone does slip something in you know who was responsible. (This is something Wheeler's technique doesn't give you).

3. Open Source, as in everyone can see and verify the previous two points for themselves.

But the sound of it Snap throws all of this away. In this era repeated of nation state attacks on infrastructure, to me that creates an unacceptable risk. Currently that seems to be a lonely position to take, but I'm betting as we get more Huawei style conflicts arise we see gradual realisation Open Source is the one of the few things that naturally gives rise to trust between otherwise antagonistic parties.

Linux Mint drops Ubuntu Snap packages

Posted Jul 20, 2020 2:29 UTC (Mon) by branden (guest, #7029) [Link]

Fortunately the state of the art has advanced since Thompson coded his Trojan. Here's a paper from 2013:

"We extend the existing formal verification of the seL4 operating system microkernel from 9 500 lines of C source code to the binary level [11,736 instructions]. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware.More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process.We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2."

https://ts.data61.csiro.au/publications/nicta_full_text/6...