On Thu, Jan 10, 2019 at 9:00 PM Thomas Bushnell, BSG <tbushn...@google.com> wrote:
> > I think the paper you linked is exciting, and actually suggests that the > hard work which needs to be done will solve the problem without a change of > language. This fits my intuition: the things necessary to take advantage of > type safety can only be automatically used with the same kind of proof work > you need to do to establish the code was fine to begin with. > > It is! It is predated by another idea which is equally exciting but never ever really tested in the large, namely proof carrying code. in a PCC scheme, a program is accompanied with a proof of its behavior according to some security policy. For instance that it is memory safe. The proof is sent as an oracle stream: whenever the proof checker is in doubt it consults the rule to apply from the oracle stream. This makes the proof small. A program is checked before it is run. In particular, this avoids the chain of trust by cryptographic signature. If the proof is correct, we can run the program. The onus on constructing the proof is on the writer of the program, or the code generator. Whole classes of security bugs can be eliminated by updating the security policy. A simpler solution was one I somewhat haphazardly tried to suggest Russ Cox on Twitter when he asked about solutions to the whole event-stream problem we saw on NPM of node.js fame. Let software be able to drop certain privileges after setup, in the style of OpenBSDs pledge(2) system call. If a module pledges itself to only ever use limited functionality, and we store this persistently, we solve many potential programming mistakes, and we make life much harder for malicious injection. This is like a poor-mans security policy, but it doesn't require the same attention to detail. Another symbiosis solution I like is the idea that we should take old software and run it, but next to a "contract checker", which is a piece of software governing the potential unsafe software. Only if the checker accepts the input, will it be passed to the potentially unsafe program. -- J. -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
