Re: [PATCH 0/8] livepatch: klp-convert tool

[Torsten Duwe]

On Thu, Oct 19, 2017 at 06:00:54PM +0200, Miroslav Benes wrote:
> On Thu, 19 Oct 2017, Josh Poimboeuf wrote:
> > 
> > Sounds nice, though I wonder what the obstacles are?
> 
> Those GCC optimizations you mentioned below and which I didn't connect to 
> klp-convert itself.

I have a bad feeling about the IPA stuff in general. An obj-based approach
is cool in a way that it still works, and is sure to work, if the IPA
assumptions that led to the optimisations still hold, but as soon as they
break, you're screwed big time. For -fpatchable-function-entries I switched
off IPA-RA, as especially on RISC there's _nothing_ you can do between
functions without at least one scratch reg. But for live patching, I'd like
the kernel to be compiled in the first place with 100% ABI adherence, IOW
all IPA optimisations turned off. Does anyone have numbers on the performance
impact?

> Nothing serious aside from that, I hope. Nicolai is currently implementing 
> C parser for kernel sources.
>  
> > > You could verify the result and its correctness.
> > 
> > Does that mean it's easier to do code review?  Or something else?
> 
> Yes, the code review.
> 
> > > It could also be beneficial if we'd like to pursue automatic
> > > verification in the future.
> > 
> > What do you mean by automatic verification?
> 
> Formal verification. Theoretically we could have a formal specification of 
> our consistency model and we could prove/disprove whether a livepatch and 
> its implementation are correct with respect to it. It is a vague idea 
> though and I personally haven't got sufficient knowledge to do anything 
> about it.

For example, if the patched functions and the fixes meet its criteria, you
could use CMBC (http://www.cprover.org/cbmc/) to _prove_ that the live patch
changes exactly what you claim to, and nothing else.

	Torsten