On 22 Apr 2021, at 13:38, Gerwin Klein mailto:kleing@unsw.edu.au> wrote:
this might sound counter-intuitive, but the glue-code proofs bring fairly low return of investment in terms of assurance vs proof effort. This is because they are about generated code, i.e. code that has systematic errors instead of random errors, because they have to assume well-behaved component code (running in the same address space as the glue code), which is only satisfied for fairly high-assurance components (i.e. needs at least a proof of memory-safety)
The one case where the glue code verification adds real value is if the connector is between two verified components, where it guarantees that the connection is functionally equivalent to a function call. As the number of verified components increase, this will become more of an issue.
So we would welcome someone redoing those proofs for the standard connectors, it’s just not high enough on our priorities (for now).
Gernot
