Received-SPF: pass (google.com: domain of linux-kernel+bounces-129828-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Message-ID: <77f5c5ed-881e-c9a8-cfdb-200c322fb55d@amd.com>
Date: Wed, 3 Apr 2024 14:25:44 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
 Thunderbird/102.8.0
Subject: Re: [PATCH v2 bpf-next] bpf: Fix latent unsoundness in and/or/xor
 value tracking
Content-Language: en-US
To: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>,
 ast@kernel.org
Cc: harishankar.vishwanathan@rutgers.edu, paul@isovalent.com,
 Matan Shachnai <m.shachnai@rutgers.edu>,
 Srinivas Narayana <srinivas.narayana@rutgers.edu>,
 Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>,
 Daniel Borkmann <daniel@iogearbox.net>,
 John Fastabend <john.fastabend@gmail.com>,
 Andrii Nakryiko <andrii@kernel.org>, Martin KaFai Lau
 <martin.lau@linux.dev>, Eduard Zingerman <eddyz87@gmail.com>,
 Song Liu <song@kernel.org>, Yonghong Song <yonghong.song@linux.dev>,
 KP Singh <kpsingh@kernel.org>, Stanislav Fomichev <sdf@google.com>,
 Hao Luo <haoluo@google.com>, Jiri Olsa <jolsa@kernel.org>,
 "David S. Miller" <davem@davemloft.net>, bpf@vger.kernel.org,
 linux-kernel@vger.kernel.org, Edward Cree <ecree.xilinx@gmail.com>
References: <20240402212039.51815-1-harishankar.vishwanathan@gmail.com>
From: Edward Cree <ecree@amd.com>
In-Reply-To: <20240402212039.51815-1-harishankar.vishwanathan@gmail.com>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
Precedence: bulk
MIME-Version: 1.0
X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1
X-MS-Exchange-AntiSpam-MessageData-0:
	=?utf-8?B?RXZqOXBBc1BTc2NrczA0ZGkzbGNVdG5iaHJwMG1XWFJuRk1DZ1VvQWhDUHpI?=
 =?utf-8?B?VWpNMGNtK1dIWUZzVXZDbk1GNlZHbElTYXMzaWZXaDZ5TWdqWVJtaDdzWjhi?=
 =?utf-8?B?UXhWU2hhWElzUHh2UDduaXRBVFRnTWZiTFlFV2pVZWgzcld5cnJaTXB2aGRU?=
 =?utf-8?B?REM4amhIMldzREVuN2dVQk9Qck5oQ2dFeXJ5Qmk5R01lRy9FUmhiTXliSDZS?=
 =?utf-8?B?OVYvZmlobGo4cnYvcE9WWE8xbitzZDM5cXR1VWI5cnFLV3d4WEh4bVJIclY1?=
 =?utf-8?B?Y1VHQzlyclBPa1F2UjB5YmNKbGpqSHBIQ0tkRVRoTGlYWFZ3cGhqdzUzMVdJ?=
 =?utf-8?B?NXNqMllCaWt6WHFzdFpJSHNBRkhBUTY0SHRQeEVnQkRMLytpZW1kSk11NkF6?=
 =?utf-8?B?MlYyVEVEK3JMcDBiTHhrSkl3OG9MQWdhZVRHTTZQTVFuNGR5cjY3V01FeUc3?=
 =?utf-8?B?OWFBdFgyY3RwMzRSVkZOOE0rMlF1c2RDOW9PZG9rN255T2hBSW9LSkMrUlpY?=
 =?utf-8?B?TCtYbjVwU0NkNWo0S1hoTjNYM2RzaXMvMmJQc0xyM1JNY0VCQjVNdmY0SE9x?=
 =?utf-8?B?Zm8vbGdIaXlmTkZVa0VXbmttaXRyU0tNc3RFWkg0Z08xemlnbW5ac0xlM0Fh?=
 =?utf-8?B?WE41SW5wdzJzUEJNR29YczhibklEdjhHbTR3MHgwb1hXcCt4NHgxb08xNGRp?=
 =?utf-8?B?Tnd0NFhBRDdzd3I0LzR5aUpHVGlaeFA5MjB4TVIzSzB3YnJEdUhhUUxjUlV1?=
 =?utf-8?B?L2VYVEFzZW02ME1Ua3J5b2hEcStPNElMemxNTm45Z1d4NUtncEpBSHpUUlRU?=
 =?utf-8?B?dS9ESnZLbzJXeHhwNVlBTWpJeWtYUVVhWjlEOHBXbERFU1Y1eUNpTlpFeTN4?=
 =?utf-8?B?aEEwWS8xVUFVZVNDYVliQytZZkt1bTFlWEFqdmpCV1Z1Ty80cXNJcjB0bkkw?=
 =?utf-8?B?WS9LY3hpUkFiMXc0d1dDS1NIY1RuNGpDanh6NjRDVEw5RHBQVzZ2V2dCSU5t?=
 =?utf-8?B?RHBMUGVWNWptaHVWeEVFZFdJTFFocVZBWDV6bnQwSGx4a3FMZzNrbkdLS2Zr?=
 =?utf-8?B?akNLQWxlYzNHMjVTTW91eGxSUUpLRzB4dXFwRTNCcksweGgyVElWVEcyYmtK?=
 =?utf-8?B?dkthT01MZzh3NmR4bGR4YjY1Z0VoTUJXYm1hMWxLTGswTndLQnNFM1k5bnN6?=
 =?utf-8?B?aUd1akN0U3NWK2R2N1ZkN0VtL2hjZTgyN3REeGhvMXJwUXdaZXAxTTR6czlM?=
 =?utf-8?B?ZzA0Z1VqTytDdWt1NS81akhkZG81emFwWnlMdzM1elJUaU8rVUkzSUlEdExu?=
 =?utf-8?B?SmJodWRFU3F0WWNDaUV3ZHBNQ2NZUkR2WGlSSmN0RXY5bXZkWFIza25tRk9o?=
 =?utf-8?B?OFlIWHlteU1rU0lwVjdKNGl3NXB0cXZWeUVCcm9kYkFuMlI1UUFLM2JYVE5K?=
 =?utf-8?B?dUw3anpDOU11RUVLWG13T3dyOWRPN1dWSHZSUUlmcFB2NnVaNXVGZXB1SWFi?=
 =?utf-8?B?aXg2NlpaSFFUeFNEc2ZhRG81YysyV0FzMUVkZ2NJWC8zQURBcnZxOW9STTJT?=
 =?utf-8?B?ZUhubXBPMzAyalZacHBYa2FqRFUwM2M5dGFscEhURWdsb2MzQzgvMHluVmpz?=
 =?utf-8?B?aFZJMGRnWStvalFYbDZVUy9kUFZrR25hd3NSMHFDNjZGb21PQWh0UnUrUFdi?=
 =?utf-8?B?dVB2UGtzcXpZcStncVBOenNIMFhLUzdTdDdveEpXRXlZMmRUOTZTRnc1V2M2?=
 =?utf-8?B?UDBoVG80WnV4c2xYSEw2QlpzOFpRZUlPWnBHSDVhWUtmZFhDbWExQVVsbGxo?=
 =?utf-8?B?MmUzTXJVMjU0dHBxK0ZwZjJRVVJMSnE4VU5pSUx6ZmdCaU5rWDdxUnFTWVNM?=
 =?utf-8?B?RXpSOUJndzlRMVM4L2lPNisrUUk4WXNLMEhXWnY5WU95SXZXT3E4dXBTWVRW?=
 =?utf-8?B?Vm1pck8xQ3V5ZHdKaUZDZEo0UVVwRlpWQ0Jrd2FtMUtHazdCbGVMRUsxV011?=
 =?utf-8?B?TmZCSndwY2x6TEs3dC92YXo2eHZNanJWWVhlZEtmZ0YxOFF3MjdDSFpzNXJ0?=
 =?utf-8?B?bnE0UHEzc2VrTEVUc1U0ZTNUcE5kazY3VnJUTDJQSXBITGh5dlNQS3lobVFk?=
 =?utf-8?Q?gslk=3D?=
X-OriginatorOrg: amd.com
X-MS-Exchange-CrossTenant-Network-Message-Id: c27d5cd7-480d-4d0b-0014-08dc53e194ed
X-MS-Exchange-CrossTenant-AuthSource: DM4PR12MB6207.namprd12.prod.outlook.com
X-MS-Exchange-CrossTenant-AuthAs: Internal
X-MS-Exchange-CrossTenant-OriginalArrivalTime: 03 Apr 2024 13:25:51.3783
 (UTC)
X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted
X-MS-Exchange-CrossTenant-Id: 3dd8961f-e488-4e60-8e11-a82d994e183d
X-MS-Exchange-CrossTenant-MailboxType: HOSTED
X-MS-Exchange-CrossTenant-UserPrincipalName: MOQrC/UydIbFkfYyskhNOR6VF56BV+tXmwWVRsJG0+BRMtQDB5H38keED9VYUTR+
X-MS-Exchange-Transport-CrossTenantHeadersStamped: SJ2PR12MB7944

On 4/2/24 22:20, Harishankar Vishwanathan wrote:
> Previous works [1, 2] have discovered and reported this issue. Our tool
> Agni [2, 3] consideres it a false positive. This is because, during the
> verification of the abstract operator scalar_min_max_and(), Agni restricts
> its inputs to those passing through reg_bounds_sync(). This mimics
> real-world verifier behavior, as reg_bounds_sync() is invariably executed
> at the tail of every abstract operator. Therefore, such behavior is
> unlikely in an actual verifier execution.
> 
> However, it is still unsound for an abstract operator to set signed bounds
> such that smin_value > smax_value. This patch fixes it, making the abstract
> operator sound for all (well-formed) inputs.

Just to check I'm understanding correctly: you're saying that the existing
 code has an undocumented precondition, that's currently maintained by the
 callers, and your patch removes the precondition in case a future patch
 (or cosmic rays?) makes a call without satisfying it?
Or is it in principle possible (just "unlikely") for a program to induce
 the current verifier to call scalar_min_max_foo() on a register that
 hasn't been through reg_bounds_sync()?
If the former, I think Fixes: is inappropriate here as there is no need to
 backport this change to stable kernels, although I agree the change is
 worth making in -next.

> It is worth noting that we can update the signed bounds using the unsigned
> bounds whenever the unsigned bounds do not cross the sign boundary (not
> just when the input signed bounds are positive, as was the case
> previously). This patch does exactly that
Commit message could also make clearer that the new code considers whether
 the *output* ubounds cross sign, rather than looking at the input bounds
 as the previous code did.  At first I was confused as to why XOR didn't
 need special handling (since -ve xor -ve is +ve).

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index fcb62300f407..a7404a7d690f 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13326,23 +13326,21 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our minimum from the var_off, since that's inherently
> +       /* We get our minimum from the var32_off, since that's inherently
>          * bitwise.  Our maximum is the minimum of the operands' maxima.
>          */

This change, adjusting a comment to match the existing code, should probably
 be in a separate patch.
> @@ -13395,23 +13391,21 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our maximum from the var_off, and our minimum is the
> -        * maximum of the operands' minima
> +       /* We get our maximum from the var32_off, and our minimum is the
> +        * maximum of the operands' minima.
>          */

Same here.

Apart from that,
Acked-by: Edward Cree <ecree.xilinx@gmail.com>