Received: by 2002:a05:6a10:206:0:0:0:0 with SMTP id 6csp1763074pxj; Wed, 19 May 2021 13:21:01 -0700 (PDT) X-Google-Smtp-Source: ABdhPJw6bB1S3LRr2KQ39U1v3DSf12MXkjcCDlvm6wI3RfEfVmPx62qMw+L/edAe4638jKNfr9dh X-Received: by 2002:a92:d6c2:: with SMTP id z2mr1043565ilp.246.1621455661825; Wed, 19 May 2021 13:21:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1621455661; cv=none; d=google.com; s=arc-20160816; b=DeutLreivugUx0gBRzNMiNjeK8AHeshpn4ZvhLdUNLcDiAdC6Djv6Rw1Hr6Fo+vf8d 29LR09lXxfEG508SGq3AaZYJbW4M21wms1mk8qPLOICuahL1LQqMSwZbcPj4s3Kjvc99 imqD3I6J798Q873p53o2z5i+2l9swH1mGMX3S1ldVEf4dzs2uJQdRKBcTpnQ1TGI4mg2 Uw8mwOFTtI77H8UXzmG9CgY0BOi6A1B98718Xm2TtG+kJYod/q1aVAV+qEdlRSpy0Py1 0yVj4YDFkzRXB6IzGZVdl5mbX7sCOSt6Xe9PWBGU3znUno4jZ0fT6P7WAOkul0c4vYKW 02KA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:dkim-signature; bh=hzUyJaz9d9LlBSmG5SweaF0Q+mql8ulPw1IIhQXoQvc=; b=WhiwSmKSC3YbzC9bD8OGHt0cRPsp4iM5dpV3I9gqAuC4k/ofapXSbXyMIznhgfKX8r I88MP8gHrzmXxNESEHZRvvFSUtI+HVxa2b0kiif0J5/fd8VclKrWRM5wqPv5JSOvxGhX ez0rtG7iEslgjRyLXf8V3RUQIyZnWt646JbldmeTYpT+rcisxEG11USBczkJunoObrqy R++lWENtn13MHjb2us9uY2+3bCHnF+alpXiVzgvljF8AbiWa3iuhUEP3uh3U40v9YJiW CcT8qK7eojXM+mZyNg3czIM+lyGfwcMHsGiEml8K5Ve4yfhP4T/pDfKwfWJC1em/1emS vkdw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@infradead.org header.s=bombadil.20210309 header.b=gNKcfrXN; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from vger.kernel.org (vger.kernel.org. [23.128.96.18]) by mx.google.com with ESMTP id c13si718095ilq.55.2021.05.19.13.20.47; Wed, 19 May 2021 13:21:01 -0700 (PDT) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18; Authentication-Results: mx.google.com; dkim=pass header.i=@infradead.org header.s=bombadil.20210309 header.b=gNKcfrXN; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231224AbhESSMM (ORCPT + 99 others); Wed, 19 May 2021 14:12:12 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35674 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229708AbhESSML (ORCPT ); Wed, 19 May 2021 14:12:11 -0400 Received: from bombadil.infradead.org (bombadil.infradead.org [IPv6:2607:7c80:54:e::133]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 01B5CC06175F; Wed, 19 May 2021 11:10:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=infradead.org; s=bombadil.20210309; h=Content-Transfer-Encoding: Content-Type:In-Reply-To:MIME-Version:Date:Message-ID:From:References:Cc:To: Subject:Sender:Reply-To:Content-ID:Content-Description; bh=hzUyJaz9d9LlBSmG5SweaF0Q+mql8ulPw1IIhQXoQvc=; b=gNKcfrXN6So0jsgE5nFvcgSNVg MxdM5VRg/o5wH82oegHXOyn38JseVneyE8CjWlbX/WLdIVCNWZgnrxj0IF7++BYH1n203jaMu7kWV 69QdiqTd6eqcGF1L+4JOkc5UpVT1E1l53QbJf3lBUutbatbi7MOS1q3z0Nh4FZ/IN7lgpf7I1k+Gg hKSHB2bdtgZOeHWTgEB5wQ7MTpquXiIVP5NkN961qkMKc/GxK7QzkNmepIlgES/BceIO2wRSa2GjY n2kt4UHnrtvyjoFcIz9CCFaLNVk9TmqL5TsME+MlD37Qz+7EfsyiNAXN5CnnqwMb8qPMCST+DQ/pT jSLYSb5Q==; Received: from [2601:1c0:6280:3f0::7376] by bombadil.infradead.org with esmtpsa (Exim 4.94 #2 (Red Hat Linux)) id 1ljQee-00FgUa-7q; Wed, 19 May 2021 18:10:48 +0000 Subject: Re: [RFC PATCH 01/16] rv: Add Runtime Verification (RV) interface To: Daniel Bristot de Oliveira , linux-kernel@vger.kernel.org, Steven Rostedt Cc: Tommaso Cucinotta , Kate Carcia , Jonathan Corbet , Ingo Molnar , Mauro Carvalho Chehab , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , "Paul E. McKenney" , Joel Fernandes , Mathieu Desnoyers , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org References: From: Randy Dunlap Message-ID: <90c917eb-f0a8-3ef5-b63d-d88c1f6919a1@infradead.org> Date: Wed, 19 May 2021 11:10:47 -0700 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.10.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 7bit Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On 5/19/21 4:36 AM, Daniel Bristot de Oliveira wrote: > diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig > new file mode 100644 > index 000000000000..e8e65cfc7959 > --- /dev/null > +++ b/kernel/trace/rv/Kconfig > @@ -0,0 +1,13 @@ > +# SPDX-License-Identifier: GPL-2.0-only > +# > +menuconfig RV > + bool "Runtime Verification" > + depends on TRACING > + default y if DEBUG_KERNEL No need for default y. There are other reasons to use DEBUG_KERNEL without wanting RV turned on. > + help > + Enable the kernel runtime verification infrastructure. RV is a > + lightweight (yet rigorous) method that complements classical > + exhaustive verification techniques (such as model checking and > + theorem proving). RV works by analyzing the trace of the system's > + actual execution, comparing it against a formal specification of > + the system behavior. And in the cover/patch 00: tlrd: should be tl;dr: or at least tldr: :) -- ~Randy