From patchwork Wed Aug 31 03:19:06 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 12960289 X-Patchwork-Delegate: bpf@iogearbox.net Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 61932ECAAA1 for ; Wed, 31 Aug 2022 03:19:52 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231801AbiHaDTu (ORCPT ); Tue, 30 Aug 2022 23:19:50 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:57172 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231279AbiHaDTn (ORCPT ); Tue, 30 Aug 2022 23:19:43 -0400 Received: from EUR03-DBA-obe.outbound.protection.outlook.com (mail-dbaeur03on2042.outbound.protection.outlook.com [40.107.104.42]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 37F3AB532B; Tue, 30 Aug 2022 20:19:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=L7A1debJy/RqC3xKmwZBBcLX1PZT9GV14GOhU7TXjFCe+7GK2QEJMaGs2lb5AR0fQU/chYLi8N98KyvmogYmVu3Kbtx8e8TyHarguVOndW8zBWU912jvU0l+ZutX9lUroknxkc/mYTqk9QtbN2DtA8aTXi2ap0lroIxGKy1RdiE8+XCRn+j34pY8eBQXnGCu8sO50BclXcMABDAU1ykcwrr77QbfikwpO86OJPK+X3VSSBugqLxu1Hq5GeFYxH/I1Cy1id2v7jQpJY1hrIRTSv9cbtRINuVcNxsoKR7n4m9gHZEjq0SfAyaPlPeYJn9A7NiW/GHfhYhGY+5QiDbH3w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=F5x4I3LevNmwk45Oba9a+3ZqWAENvhlIreg22lv7WHo=; b=AbsOW7CO+/RVWRAcil1Z6UjyoGlHTkChdrVAgQD8xO55lQNtaTrCSvoVtDC1jz2nSwmOeJWHiPdRiPn7A7OvHOZaVOjWLoIroKyF3sB6JjTW4D85Ug2saj/n4LtPxoZxc/NYG6oXuJHr9lCyy4ho4Tz1h5ltU0uVM+cD4xz37xPf4AAshhUy3wrtb01zVOoT1HHwN5GwGmFvXJRM01RZvS5SlRsZLG13euPK1gzQqcoigBxOr1IYAMI2WUg9ydTRz5XuNf9AnisL0w5i+Svk1jXAcvEZEVNl4bSoNYeiQ1IyatYpyo9wyIYQty9vV2UTuANQPRfGmYWbVWbwcCMwRw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=F5x4I3LevNmwk45Oba9a+3ZqWAENvhlIreg22lv7WHo=; b=fNHrjt+jZQN+x5o0KILRgHaR7PF7633jYldEtyJwlivIDk172766te2OhkXDst4d9CBCWo/rcd+hvSrRA2gRdRGVy8z9u8JhjYt/eIoN4LT5LK+bZR5QeeSgBrZu1ODleGeZ3WcvHEqLZFQOPC7EPdGlfrSb1/J0VqgiSA1F0jcoA+RuD8amr/kFZt12pQ5oQJAZCK4IG6JdhDgvgOQD4EsadSzDGlZBOHw4yOjsnjkchvZRyOIKfRTR8SB9rDfLg54KVTwzNbTn800Ar/U2NB7Aka9OGNuIfe5TVVHMJswh21JsowunYcqB7GgjhN5ejJZQ+g08rK31lF3ELPlVkw== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from DB9PR04MB8107.eurprd04.prod.outlook.com (2603:10a6:10:243::20) by AM5PR04MB3009.eurprd04.prod.outlook.com (2603:10a6:206:10::32) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5566.21; Wed, 31 Aug 2022 03:19:35 +0000 Received: from DB9PR04MB8107.eurprd04.prod.outlook.com ([fe80::f95c:9464:9bc0:f49b]) by DB9PR04MB8107.eurprd04.prod.outlook.com ([fe80::f95c:9464:9bc0:f49b%9]) with mapi id 15.20.5588.010; Wed, 31 Aug 2022 03:19:35 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org, linux-kernel@vger.kernel.org Cc: "Alexei Starovoitov" , "Daniel Borkmann" , "John Fastabend" , Shung-Hsi Yu Subject: [RFC bpf-next 1/2] bpf: tnums: warn against the usage of tnum_in(tnum_range(), ...) Date: Wed, 31 Aug 2022 11:19:06 +0800 Message-Id: <20220831031907.16133-2-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.37.2 In-Reply-To: <20220831031907.16133-1-shung-hsi.yu@suse.com> References: <20220831031907.16133-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: FR0P281CA0113.DEUP281.PROD.OUTLOOK.COM (2603:10a6:d10:a8::13) To DB9PR04MB8107.eurprd04.prod.outlook.com (2603:10a6:10:243::20) MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: d2d38ff4-a488-4cee-9379-08da8affa0e8 X-MS-TrafficTypeDiagnostic: AM5PR04MB3009:EE_ X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: jCwQ8hCZLc5tRDJFfP+dOliD6p2cV5k7i87DQ3DixyGpv0d6bm0F0j99ulLKVEZEF5rOBCa2YTBe5/L+wug3JR3HeqUcrGQV03ttIczylNB9sF9FWaoMMRqVm+jrBic806TKQIuj7/iIONrtKYbgBaOFLjI4IuMno9UaGhM7FaXwX3WWTPiKvJUrLl217ESYrXgwDNYY6Q22uEp688WyLAD9vS26TAEarD4BYEYyYICM2XICwbuNFD5VP5LNokV8peNp0CaZa6oaNRhlFTdlxsctqMgkkUBOu2BW+JLKE/7gLmQtUTceDlY/SYvOkXa+7/BBynE1oNhbXiNugYcQaeQGj3B9KfOXSaOceTeyRXszEn5xIG06ZFeGdsXPCI86OysjAX3ANgnqMpP7fkEZWo2IOngGTQdnLid1i7KrP4RPa6Opoj4ehgWTQiaJfIJ1NQF6zW9ddTKTMcg833UdFyU5NLFeJefWEyK3ZtViPHqB0E6VqDYGvKGQ33B+RfAEgEW730XAoA4QH7zz1/CNji+RdcJcE57vKE95WI5j2T0xe9QfLm/5aco0nsgWeKct8goPg/UpfFdD9ZTFskaGuiMBmihG3uTPnQIZ1pjaFdr47bbdM9WUYZGNin6AdAv/D+GcQfb4nI6U7uth89EXsOXZQMZkueRrKa+3h90xMBffUyDk+VPY/TpCoe+bm6DN/YEI2wveYSFG6X+0zUa2l/1z+TbCesWFrvkWzbBRVrOT6z65N+rC8/Nn/x+plT5d3mLt+RxO2eltVz0LNNbPNw== X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:DB9PR04MB8107.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230016)(346002)(396003)(376002)(39860400002)(366004)(136003)(38100700002)(26005)(6506007)(2906002)(107886003)(6666004)(2616005)(6512007)(186003)(83380400001)(6486002)(86362001)(8676002)(66946007)(316002)(66556008)(66476007)(54906003)(4326008)(36756003)(1076003)(966005)(8936002)(41300700001)(5660300002)(478600001);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: YjTWmJ82Z6XTvuxofdJYOq3i+V0ZjuWEryJfvlNLLX3JgALAHvpUSDgPgBm0jlUeHznXgB/J33ZDd/vMCbOsnmzc0jZf/fkBRToTQxK690hFpfejcX+1FKxKZwwwjzHnOs7wafaqJwg9KairdUU/fDj2rEnBkEiwM4Je++LYrIvAXm1IW8SYufRrcTO6aEQAtHPbK+cVHX8p8hboXMICphw9xUCbivsnXrELcRqrKM7z9mtsQInwdWBvY+bdWYCIQydbXxIltzoIevGohaLJPO5ZolQXnpNgqfm3mR9JeZ8fkocWc6El00Hzr8xIAPgDyYV7lL1OLfNc0lZONkU5aplvnJZD/z3du62XzXseIojFNQbmcLb0MDjgVXuzTB8hPNnDrrDJcmwckkCvUheeIlmeNByGfC4CLFTO4xKT0+qf1qwv0vzED4bJjyJNM2GFFPG2ZOoUSI+Janr5LsXQqUVpmqkegdun3R7/2KvAIzCqDH+XgQ9fWG5pECzjpEkdbJhXOwnheBTCUHIR6+qQo3ophkUZRXKC0NsbsrASrQFBzY5aUwynwj3ltDVe4SSDtFrHXWLAtuVivLKMkIOOz00Sm4ILQBjU3zwEvtFoDgt0y+Ek+kk7qhkte3cWut84RZO4Uq9H310sEYmNKyMkHPhgeaW3EQ6g6v1+QT/FwMkCeLhL3e01zruzk8EBHSIv/sLx+jZso3941SNQTCQb/9TkWAV9+IN5z243NiUmNMMt9nw9wNqlp145aGMshS8nhyZ9AJaR/6jo5TEdZ31Yme/p0U4xVMfglpuvChmnM6McQl/S9Jrv9LaEcp3jGvaSx3WB9i9JMtffYuCfG9RqY2V9aWcH4MZWoxPR1vzf2nIL8dYYbmYHveGran5IVcUp91sXYasSPhmlH9GsgnhHpqqxXgF4vKSfSYWkWVTcQ2VyvSGZl1FXRk0Qh/GzNEQg4hE2R2g6oUyEQ/LnhHpUSp37zRl/LNCptIVkuQ11k2jJqM2szR1TBtA4TTrIA6ev1kF3KijW34+8RKc9uwVg7HwsrMAbuGxbpiYasTNfeHm0Ez3nqurR5C4WbmniNx6RRHuDjn4zqpgIm4cLuhI3y8bRY01k9rDOnNTj8friN88UG9vN9j8apNz+b31oaLp2U7su4+aYz6Ct21N2zyOj6uf2XG1gUjvz7uwUPXS+dBKzGjxR10nz8fN058Hy5M1BLqQ+AUqnNQ5haYa1TxpyIGlS6CeCzp7/lhrdfHUsNmt0pjHssnh/QG2GIKCTArJwRSwcZCALKdJvAy17QC1/sM18RClG2PijLNXML4mza7dG3LwDOViooX5Z0P0nGtN8fta6a3U8/0v9DF4tKsNj1Kmue333p94ID0SuSC52et17qNReB9sFKkkH9qjVjcnnZD6chHaH2gnrLQVSGH3XqQTaDIUxcXzx7GVFgUPAEF+tCHnX8SEER5bn0CYpsyDKywAHiUB7hvW3O8yq6JoSWO+ZsI2h00964dL0X8cjpzV9gt4KeioDqSjqs/yKrIocyeq5XjgRCjpEGoHrsRR6cCQlZ0rke0oBGZrjkm5yvVmz7WxKFDJjNefv64qB4j0F X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: d2d38ff4-a488-4cee-9379-08da8affa0e8 X-MS-Exchange-CrossTenant-AuthSource: DB9PR04MB8107.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 31 Aug 2022 03:19:34.9267 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: n3XzMI7+6XY2WpePvHdm4G4vQ0ankg0wjrKB1CDrQC+KhwK2JHV8L9qpkiMu3aHhlUYmdVvecQmI6Hu3CXXn0g== X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM5PR04MB3009 Precedence: bulk List-ID: X-Mailing-List: bpf@vger.kernel.org X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Commit a657182a5c51 ("bpf: Don't use tnum_range on array range checking for poke descriptors") has shown that using tnum_range() as argument to tnum_in() can lead to misleading code that looks like tight bound check when in fact the actual allowed range is much wider. Document such behavior to warn against its usage in general, and suggest some scenario where result can be trusted. Link: https://lore.kernel.org/bpf/984b37f9fdf7ac36831d2137415a4a915744c1b6.1661462653.git.daniel@iogearbox.net/ Link: https://www.openwall.com/lists/oss-security/2022/08/26/1 Signed-off-by: Shung-Hsi Yu --- include/linux/tnum.h | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/include/linux/tnum.h b/include/linux/tnum.h index 498dbcedb451..0ec4cda9e174 100644 --- a/include/linux/tnum.h +++ b/include/linux/tnum.h @@ -21,7 +21,12 @@ struct tnum { struct tnum tnum_const(u64 value); /* A completely unknown value */ extern const struct tnum tnum_unknown; -/* A value that's unknown except that @min <= value <= @max */ +/* An unknown value that is a superset of @min <= value <= @max. + * + * Could including values outside the range of [@min, @max]. + * For example tnum_range(0, 2) is represented by {0, 1, 2, *3*}, rather than + * the intended set of {0, 1, 2}. + */ struct tnum tnum_range(u64 min, u64 max); /* Arithmetic and logical ops */ @@ -73,7 +78,18 @@ static inline bool tnum_is_unknown(struct tnum a) */ bool tnum_is_aligned(struct tnum a, u64 size); -/* Returns true if @b represents a subset of @a. */ +/* Returns true if @b represents a subset of @a. + * + * Note that using tnum_range() as @a requires extra cautions as tnum_in() may + * return true unexpectedly due to tnum limited ability to represent tight + * range, e.g. + * + * tnum_in(tnum_range(0, 2), tnum_const(3)) == true + * + * As a rule of thumb, if @a is explicitly coded rather than coming from + * reg->var_off, it should be in form of tnum_const(), tnum_range(0, 2**n - 1), + * or tnum_range(2**n, 2**(n+1) - 1). + */ bool tnum_in(struct tnum a, struct tnum b); /* Formatting functions. These have snprintf-like semantics: they will write From patchwork Wed Aug 31 03:19:07 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 12960290 X-Patchwork-Delegate: bpf@iogearbox.net Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 7EB79ECAAA1 for ; Wed, 31 Aug 2022 03:20:16 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S232220AbiHaDUM (ORCPT ); Tue, 30 Aug 2022 23:20:12 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:57168 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S232190AbiHaDTs (ORCPT ); Tue, 30 Aug 2022 23:19:48 -0400 Received: from EUR03-DBA-obe.outbound.protection.outlook.com (mail-dbaeur03on2049.outbound.protection.outlook.com [40.107.104.49]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 0F41BB5E57; Tue, 30 Aug 2022 20:19:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=STtJGVIR1xLHeUAxGQzi35NBk7a87kFzWVlXp5GWCqq/xuCOUncBwAOJp2pYoj51rOV//TM3g8TH0BKuui2HTLhNfkh3awt2L2aaAe19JZNP9267k5Ab07WyzG4p4liCQoEXiCnRTXJsBS2BBZ244j2inxbnViuY87kTwbkrLvtSwOZYAO93kmEDUg6EQ0SpvNFKDBzGUBwN33uoZp++CuGO5A6rRIUBOR23MFZbi5uD/gICE5c6Az0zh4LTLyeEH+win+lAO0iVbXukYSxl+L2U0tH8C5c9ib8ug2ZJEA0jvEOCb/1+g4K9cPStKkVN0Vy4RNzQ33mPgmzHReaX/Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=aOm0RDquLbflUmHQHR5CF8LlJjH3HMMpHcgKCE/9oVg=; b=VrWygwL85UkzaTOKXkU4iKUy+vJd5R+EdCYk4vZrvejeULcRWn46EpKaeJg9UQNlju4HflvOAaxH9+eJzw4y/GFwqecMOrBvR17E+M5yKX+y1kOFBWMR0jt/nbftmC2/JYaP0bL6DueVSYhUjZ5rZJLGubFV29S43ag/+jP5hJMDHNpmA6o6Iqb7R3Zy6S6TtqimLlTTO3EdjblmfGRU+ZcmiQyLss1yCUIGMlAkXnHAJlqR8PjVZ/YqmfG5odn90MDAxZhG0KLkxr8XMnIqfB1iAq6XbGyRsEt44WAlodrNO6emSsmQ0BMs2jozCTJnjN5/KccQElQvq3ar8FW2/A== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=aOm0RDquLbflUmHQHR5CF8LlJjH3HMMpHcgKCE/9oVg=; b=xc1nqoyN+DO+svtmhmlQ7/vsaFWKzMgzPn23hZ8olPMG+3MIXtflzwVv67wQBvJYKVPId4QbeWZY/eAfbuMLAAjFo2DQc+hT4ZsY+PS3D2sItl8PNghoAOj/4UW/o2KEyyZIzSxrnkrv5qLrS8WoaPLy/H86WYzaxYoXHYzNP0bLR85RwzYfHrbI7JHjX2ewLSCO4eA2gX1fBh3a1DNlGQZmMx8Q/c29UlhNDOdZHM0+2gIFzlfy0bbG7X/Lm6Z5cRe2JFS9Jy2OV+yZm63hFLFQCEiLtB6YfdaqkDogks3+p0xoWRq6bXlaFUz9ckC5L9L4M+wPz9RZDV0sYdazGg== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from DB9PR04MB8107.eurprd04.prod.outlook.com (2603:10a6:10:243::20) by AM5PR04MB3009.eurprd04.prod.outlook.com (2603:10a6:206:10::32) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5566.21; Wed, 31 Aug 2022 03:19:40 +0000 Received: from DB9PR04MB8107.eurprd04.prod.outlook.com ([fe80::f95c:9464:9bc0:f49b]) by DB9PR04MB8107.eurprd04.prod.outlook.com ([fe80::f95c:9464:9bc0:f49b%9]) with mapi id 15.20.5588.010; Wed, 31 Aug 2022 03:19:40 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org, linux-kernel@vger.kernel.org Cc: "Alexei Starovoitov" , "Daniel Borkmann" , "John Fastabend" , Shung-Hsi Yu Subject: [RFC bpf-next 2/2] proof for the safe usage of tnum_in() Date: Wed, 31 Aug 2022 11:19:07 +0800 Message-Id: <20220831031907.16133-3-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.37.2 In-Reply-To: <20220831031907.16133-1-shung-hsi.yu@suse.com> References: <20220831031907.16133-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: FR3P281CA0086.DEUP281.PROD.OUTLOOK.COM (2603:10a6:d10:1f::13) To DB9PR04MB8107.eurprd04.prod.outlook.com (2603:10a6:10:243::20) MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: 4e87b229-89f6-4ed7-6eac-08da8affa3d3 X-MS-TrafficTypeDiagnostic: AM5PR04MB3009:EE_ X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: PqQAaUnDBP6H+ymi8nkljoDkTZ4bj7HQRYbAXA7VGLnLP65szbrqoV3j+5Cg6DSX+J90qP50pS0M/QPiBtQRLkVUHsGD2Yt41BVL9aCyA/glefi2ZFh+Fv4gMQyhyXxT9kU5sOcl7kBt3ACVwVNh0cJRppzggPiKKjw9Zn0UnHBgBxhKWWWhLSeZTZoeEzVhtRQJYeLgSmN3xxzocoOvOCij4eABLHWQM153Qy3sAZ5iY/yf9w5znPpQjsiTeG3Qd0EUF8z9l7UjKkCb9etypXcNNDAjOBdy5SduMypYcq4Nux3LGCv04AZZhEtM9w76i7MghjEcrx+fbbwIYo9sPVNQRBmJMCqPVE7Sjd0GH4y8zx6NTaeglxTdSgjQHJj9FIPUmbXdxa9gv2FUrlfpl8W6xWvz+XgK21zoP5lYFK7BMmAgaJbVVnZjySIdSvbsXWmYbdAv9dNL+7NywwPglrVMPZVUjBjM2LJ6wXv2HiYcgkUIqu5tOJusjL99PKT5Ntx0ENe9hvhwULXPNAZOqtRTX6YfVm42z+oUOKL4cqZjXKH0+OiTxx/dKmZ+uFQ+ZUK6BuweSncKKUe96OGC2/mrF3DPLj245Mr5Pt2fHYmnWhDAHFceuaabS+U1hHo1HPsrsN6Cf2cI1zTHL3ZEuxwEJZieFJ26wZguXofow0C0Q1Sk/kQ675AHPIrvqCBq/l9dGwsguyX2nUdA4GftlBkBe7mPfg2yd+WPUjJKQU3eefOyeoMstpN4EoMcI8VbW1oeA41uMNTjF1asY1wc++/8YAS7UU9l713NWiawR7I= X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:DB9PR04MB8107.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230016)(346002)(396003)(376002)(39860400002)(366004)(136003)(38100700002)(26005)(6506007)(2906002)(107886003)(6666004)(2616005)(6512007)(186003)(6486002)(86362001)(8676002)(66946007)(316002)(66556008)(66476007)(54906003)(4326008)(36756003)(1076003)(8936002)(41300700001)(5660300002)(478600001)(461764006);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: kne0H212/9lpABBMtrVvbUb1WEwKyRthdI4PdperBVh/pLAtexcUwbiscAGYw9E7viGdVAXPvJMH2a04OTX9jWnIzHxV5i49/vd3ZJitsZm2BBP9vu5K9GtgGG34UR+Sd51cE3l5aJG9iHWEoxutsph1CpHIkVQ6NhPAXYmWavvMe7dKza8ncNQDkViYiSK03XGPyyj8TIMfBxxLFIpjUWJsxv1TfJA82QEv87i3drXBqPiurEIas7cVa3g+wdgmrxI4U3Hp/8jTTrFDougN1dDqKVSNhHBxZITnHdiR+5lKJAqC81PWrmmDfZozXojzDXmrdEzhH3p+ik0qXyyVxZ7XUNkRyZ4oBdIHcVFoRuNxD7HUL1f8Gtrk74odjLo3/UE3IpZE1lDS7OSjfhrY2V35iL4fSv3Q4fCxmiV0SxUH2S7VyT/Vr/wVuHR+N5xNLBx9o1PbaQjJdBIVsVVd2OQ6LaM6AujGZEQhZE5uxUp/yd52SZtaqCSxjHXZLOrlZUomx64uynNg0qwZJYTxXx13OOVuZOGB+nQisvZOptfJg8pzL9LWR03sJFfuYBUl8cGBw7/V6zAbSE46Yq3oYONwHBD0MH9tsPcG0oHVsr00fImN8xl998V0sJ6qH9SZgyPph6oHCXRl7Afwtj5pbxGGSyBv8G1IvWrTSyLq6OQqA6ArbUmglLkoU2RYG+ukfW3TuDzJvp26RZdyo4leUQf2oonPnTLe76phS43N6UsY46oqqCTzFZiG4hiHlW61Hx7hcNqCVk7T1CTWCJGlWFNUmRxWszbwdDYfA7EuVrxE9Pzyii04t0kHpIly5iv0zFUO2q/NEHNgfFM3bhjzkbfWnUdkC4fNJIFTbtKvuC3bio9hrJdLdDj9SWaWqtk8ErJXDEVBboyn4hP7gdFeSXVJxFW90W1k7Sy3tR5RK/ln1JOmZ4ShurLaxQEt2NWCWrvih/VhpPiaTKutfekSObuiKlo14k1FRMLGHLuMJhonbZEjozqkRq1hHyQ9yT0CObM3hxHMKSTOJBw0IhWvIeK+HJbmL7ZcU++ovz0ctFTII/7nRRPoJVtepLBgORc4GQR7NSVOlN9b7XWsv8V/5KxiPYz7ffe6Qts5D2DxuxM2tnqfLZSYAHoIwKsQVJREimrn6LqqUPIJz0qLOeF5X0Bpne3QMi24NdfAQps1UvFnwr8ptVAEHUEMIxv8OAsaidmxvAR0SlcOWS3kl6nrCMeKdMMZyiBsW7Kk/PIWrssnbRQbDGVI83i1pBDWLof9k2sNK1A/QWuIkQ7be56cW6obP95X6g58kldPBBSNMjRaiKclzWBZEAZeoJJtxqoOa/jLxMHv5JlwpUjRxIyX67gK8d0WAyANSmK01Lwb/OVwixIwsq7c4tTXEgcyAfmQPEf0M5K/IUnuWNzMeQbuAZ7wXg6xlNQHtdxUNidMFur/2wIx47hivzMF9JOmYbMVIMwy+zu76EpshasVQ7xIV9QGN26lVu5KlZDkcAHveTWsf9Db06gwgCqPVP9RFdBPGH6EbTiqR9QsxEmmaOWh0pBRNuUKYusjr13sovy0C4H3FfEXX8JoX0/PUtnQZ99P X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: 4e87b229-89f6-4ed7-6eac-08da8affa3d3 X-MS-Exchange-CrossTenant-AuthSource: DB9PR04MB8107.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 31 Aug 2022 03:19:40.0088 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: 3CRjsrHSiobIxYf0amfklHH5gye45cecfSck2We3Ufx8L4enX5nUASmwwUvr/GoJaW2J4qgYuhCAFqK2urwgjA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM5PR04MB3009 Precedence: bulk List-ID: X-Mailing-List: bpf@vger.kernel.org X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC This commit is not meant to be merged, merely as a display of proof about the claims in previous commit that tnum_in() can be trusted when used in the following form: - tnum_in(tnum_const(), ...) - tnum_in(tnum_range(0, 2**n - 1), ...) - tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...) Note that this only proves that tnum_in() can be trusted when it returns true, and proof nothing about whether it's trustworthy or not when it returns false; the latter is still being worked on. Signed-off-by: Shung-Hsi Yu --- tnum_in.py | 158 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100755 tnum_in.py diff --git a/tnum_in.py b/tnum_in.py new file mode 100755 index 000000000000..e4567bda51c4 --- /dev/null +++ b/tnum_in.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +# +# A proof on the property of tnum_in(tnum_range(a, b), ...) using the Z3 +# theorem prover +# +# Requires the z3 Python module (aka Z3Py), which can be installed with the +# command `pip3 install z3-solver` +# +from uuid import uuid4 +from z3 import And, BitVec, BitVecs, BitVecVal, Extract, If, Implies, Or, ULE, UGT, ZeroExt, prove + + +class Tnum: + """A model of tristate number use in Linux kernel's BPF verifier. + + Largely based on the "Sound, Precise, and Fast Abstract Interpretation with + Tristate Numbers" paper . + """ + SIZE = 64 + def __init__(self, val=None, mask=None): + uid = uuid4() # Ensure that the BitVec are uniq, required by the Z3 solver + self.val = BitVec(f'Tnum-val-{uid}', bv=Tnum.SIZE) if val is None else val + self.mask = BitVec(f'Tnum-mask-{uid}', bv=Tnum.SIZE) if mask is None else mask + + def contains(self, bitvec): + # Mask out the unknown bits, if what left is that same as value, then + # this that integer is represented by this tnum + return (~self.mask & bitvec) == self.val + + def wellformed(self): + # Bit cannot be set in both val and mask, such tnum is not valid + return self.val & self.mask == BitVecVal(0, bv=Tnum.SIZE) + + +def is_power_of_2(n): + return And(n != 0, n & (n-1) == 0) + + +def fls64(bv): + size = Tnum.SIZE + num = BitVecVal(0, bv=Tnum.SIZE) + while size > 1: + half_size = size // 2 + h = Extract(size - 1, half_size, bv) + bv = If( + h != 0, + h, + Extract(half_size - 1, 0, bv), + ) + num += If(h != 0, BitVecVal(half_size, bv=Tnum.SIZE), BitVecVal(0, bv=Tnum.SIZE)) + size = half_size + + assert(size == 1) # Size is now 1 + num += If(bv != 0, BitVecVal(1, bv=Tnum.SIZE), BitVecVal(0, bv=Tnum.SIZE)) + return num + + +def tnum_range(min_, max_): # Don't shadow built-in min & max + """tnum_range() implementation modeling what's found in the Linux Kernel""" + chi = min_ ^ max_ + bits = fls64(chi) + delta = (BitVecVal(1, bv=Tnum.SIZE) << bits) - 1 + too_large = UGT(bits, BitVecVal(Tnum.SIZE - 1, bv=Tnum.SIZE)) + + val = If( + too_large, + BitVecVal(0, bv=Tnum.SIZE), + min_ & ~delta, + ) + mask = If( + too_large, + BitVecVal(-1, bv=Tnum.SIZE), + delta, + ) + return Tnum(val=val, mask=mask) + + +def tnum_in(a, b): + """tnum_in() implementation modeling what's found in the Linux Kernel""" + return If( + (b.mask & ~a.mask) != 0, + False, + a.val == (b.val & ~a.mask), + ) + + +# a, b, and x are integers which could be of any value +a, b, x = BitVecs('a b x', bv=Tnum.SIZE) +assumptions = [] + +t = tnum_range(a, b) # Any possible range we could get out of tnum_range() +assumptions += [ + ULE(a, b), # a <= b +] + +st = Tnum() # The second argument can be any tnum +assumptions += [ + st.wellformed(), # As long as it is a valid one + st.contains(x), # And contains the number x (that could be any integers) +] + +condition = [ + # When tnum_in() returns true + tnum_in(t, st) == True, +] + +print("""\ +Trying to proof that tnum_in(tnum_range(a,b), ...) can always be trusted when +it returns true... +""") +prove( + Implies( + # When using tnum_in(tnum_range(a, b), ...) + And(assumptions + condition), + # Try to prove that we can always trust it when it returns true + # That is, all number that the second argument can represent (i.e. x) is + # inclusively between a and b + And(ULE(a, x), ULE(x, b)), + ) +) +print("") + +# Additional constrains, namely that the first argument need to be in the form of either +# tnum_const() +# or +# tnum_range(0, 2**n - 1) +# or +# tnum_range(2**n, 2**(n+1) - 1) +additional_assumptions = [ + Or( + a == b, # since a == b, tnum_range(a, b) == tnum_const() + And(a == 0, is_power_of_2(b + 1)), # b is 2**n - 1 + And(is_power_of_2(a), b == (a << 1) - 1) # a is 2**n and b is 2**(n+1) - 1 + ), +] + +print("""\ +Trying to proof that tnum_in(tnum_range(a,b), ...) can always be trusted when +it returns true, again, but with constrains on a and b, namely the first +argument of tnum_in() must be in one of the following forms: +- tnum_in(tnum_const(), ...) +- tnum_in(tnum_range(0, 2**n - 1), ...) +- tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...) +""") +prove( + Implies( + # When tnum_in() is used in the form of + # tnum_in(tnum_const(), ...) + # or + # tnum_in(tnum_range(0, 2**n - 1), ...) + # or + # tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...) + And(assumptions + additional_assumptions + condition), + # Try to prove that we can always trust it when it returns true when the additional + # contrains above is inplace + And(ULE(a, x), ULE(x, b)), + ) +)