<feed xmlns='http://www.w3.org/2005/Atom'>
<title>linux-toradex.git/kernel/bpf/Makefile, branch master</title>
<subtitle>Linux kernel for Apalis and Colibri modules</subtitle>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/'/>
<entry>
<title>kbuild, btf: Expose vmlinux inline BTF through sysfs</title>
<updated>2026-10-11T14:18:06+00:00</updated>
<author>
<name>Alan Maguire</name>
<email>alan.maguire@oracle.com</email>
</author>
<published>2026-10-09T11:23:20+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=672981f4aec1d0131761aec60298312464bd7a50'/>
<id>672981f4aec1d0131761aec60298312464bd7a50</id>
<content type='text'>
Expose BTF inline-location information from vmlinux .BTF.inline
sections in /sys/kernel/btf as vmlinux.inline. Embedded vmlinux
inline BTF supports read-only mmap().

Provide runtime support for a module-delivered vmlinux inline BTF
carrier. Its link record binds the carrier module name, BTF size, and
SHA-256 digest to the running kernel before its data is made available
through a lazy vmlinux.inline sysfs attribute. The carrier is handled
before ordinary module BTF registration, so its incidental .BTF data is
not exposed.

Make CONFIG_DEBUG_INFO_BTF_INLINE tristate. When configured as a
module, retain vmlinux final split inline BTF for
btf_vmlinux_inline.ko instead of embedding it in vmlinux.

Reserve .BTF.inline.link in vmlinux and extend the final
resolve_btfids patch pass to bind btf_vmlinux_inline to the raw
vmlinux.BTF.inline payload. This preserves the normal built-in
configuration while allowing the large inline BTF payload to load on
demand.

Normal module inline BTF is handled separately, after its
references have been relocated against the final module BTF.

Signed-off-by: Alan Maguire &lt;alan.maguire@oracle.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009112324.1442319-4-alan.maguire@oracle.com
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Expose BTF inline-location information from vmlinux .BTF.inline
sections in /sys/kernel/btf as vmlinux.inline. Embedded vmlinux
inline BTF supports read-only mmap().

Provide runtime support for a module-delivered vmlinux inline BTF
carrier. Its link record binds the carrier module name, BTF size, and
SHA-256 digest to the running kernel before its data is made available
through a lazy vmlinux.inline sysfs attribute. The carrier is handled
before ordinary module BTF registration, so its incidental .BTF data is
not exposed.

Make CONFIG_DEBUG_INFO_BTF_INLINE tristate. When configured as a
module, retain vmlinux final split inline BTF for
btf_vmlinux_inline.ko instead of embedding it in vmlinux.

Reserve .BTF.inline.link in vmlinux and extend the final
resolve_btfids patch pass to bind btf_vmlinux_inline to the raw
vmlinux.BTF.inline payload. This preserves the normal built-in
configuration while allowing the large inline BTF payload to load on
demand.

Normal module inline BTF is handled separately, after its
references have been relocated against the final module BTF.

Signed-off-by: Alan Maguire &lt;alan.maguire@oracle.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009112324.1442319-4-alan.maguire@oracle.com
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Compute scalar evolution expressions for loops</title>
<updated>2026-10-09T20:29:14+00:00</updated>
<author>
<name>Eduard Zingerman</name>
<email>eddyz87@gmail.com</email>
</author>
<published>2026-10-09T10:47:51+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=1501b536818b99a643842296a062019d221716f7'/>
<id>1501b536818b99a643842296a062019d221716f7</id>
<content type='text'>
Assign algebraic expressions to loop variables (registers and stack
spills), describing how their values evolve across iterations. These
summaries provide symbolic input for the subsequent widening patch.

The algorithm draws on ideas from the following papers:

- "Symbolic Evaluation of Chains of Recurrences for Loop Optimization"
  Robert A. van Engelen, 2000
- "The CR# Algebra and its Application in Loop Analysis and Optimization"
  Robert A. van Engelen, 2004

The analysis proceeds in two phases:

- Compute expressions for one symbolic iteration: start each variable
  with a reference to its input value, apply instruction effects and
  join expressions where control-flow paths merge.
- Convert the resulting backedge updates to recurrences at the header,
  then substitute these recurrences into expressions at the latch.

Analyze loops innermost first. Within each loop, visit blocks in
topological order (reverse postorder, with backedges ignored and nested
loops collapsed). Treat each nested loop as an opaque operation:
preserve its invariant values, forget the others and continue at its
exits, without expanding its iterations.

For example, using 64-bit arithmetic:

    0: r7 = 5;
    1: r6 = 0;
    2: do {                // header
    3:     if (r6 == 1)
    4:         r7 = 10;
    5:     r6 += 1;
    6: } while (r6 &lt; 3);   // latch

Expressions use symbolic inputs r6 and r7; the concrete values from
lines 0-1 are supplied later by the main verifier.

First phase:
------------

At each instruction, an environment maps register numbers to their
current expressions. Transfer functions update this mapping, while
joins merge the environments arriving along different paths.

For illustration, follow each branch separately to the backedge:

- At 3, take the path skipping 4: r6 = r6, r7 = r7.
- At 5, transfer(r6 += 1): r6 = r6 -&gt; r6 = (+ r6 1).
- At 2, the first path contributes r6 = (+ r6 1), r7 = r7.
- At 4, on the other path from 3, transfer(r7 = 10):
  r7 = r7 -&gt; r7 = 10.
- At 5, transfer(r6 += 1): r6 = r6 -&gt; r6 = (+ r6 1).
- At 2, join the two paths' contributions:
  join((+ r6 1), (+ r6 1)) = (+ r6 1) for r6;
  join(r7, 10) = (any r7 10) for r7.

Equal expressions stay unchanged; different expressions become ANY
alternatives. These summarize one iteration, without unrolling the loop.

Second phase:
-------------

The update r6 = (+ r6 1) says that each iteration adds 1 to r6.
Repeating this update n times gives r6_entry + n, a linear recurrence.

- At header 2, r6 = (+ r6 1) becomes (linear r6 1), meaning
  r6_entry + n, where n counts iterations from zero.
- At latch 6, substitute this recurrence into (+ r6 1):
  (+ (linear r6 1) 1) simplifies to (linear (+ r6 1) 1),
  meaning r6_entry + 1 + n.
- At both points, r7 retains (any r7 10): either its entry value
  or 10. ANY records alternatives, not numeric ranges or the path
  conditions selecting them. Unchanged variables retain their inputs.

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-33-bcba9bc53ac9@gmail.com
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Assign algebraic expressions to loop variables (registers and stack
spills), describing how their values evolve across iterations. These
summaries provide symbolic input for the subsequent widening patch.

The algorithm draws on ideas from the following papers:

- "Symbolic Evaluation of Chains of Recurrences for Loop Optimization"
  Robert A. van Engelen, 2000
- "The CR# Algebra and its Application in Loop Analysis and Optimization"
  Robert A. van Engelen, 2004

The analysis proceeds in two phases:

- Compute expressions for one symbolic iteration: start each variable
  with a reference to its input value, apply instruction effects and
  join expressions where control-flow paths merge.
- Convert the resulting backedge updates to recurrences at the header,
  then substitute these recurrences into expressions at the latch.

Analyze loops innermost first. Within each loop, visit blocks in
topological order (reverse postorder, with backedges ignored and nested
loops collapsed). Treat each nested loop as an opaque operation:
preserve its invariant values, forget the others and continue at its
exits, without expanding its iterations.

For example, using 64-bit arithmetic:

    0: r7 = 5;
    1: r6 = 0;
    2: do {                // header
    3:     if (r6 == 1)
    4:         r7 = 10;
    5:     r6 += 1;
    6: } while (r6 &lt; 3);   // latch

Expressions use symbolic inputs r6 and r7; the concrete values from
lines 0-1 are supplied later by the main verifier.

First phase:
------------

At each instruction, an environment maps register numbers to their
current expressions. Transfer functions update this mapping, while
joins merge the environments arriving along different paths.

For illustration, follow each branch separately to the backedge:

- At 3, take the path skipping 4: r6 = r6, r7 = r7.
- At 5, transfer(r6 += 1): r6 = r6 -&gt; r6 = (+ r6 1).
- At 2, the first path contributes r6 = (+ r6 1), r7 = r7.
- At 4, on the other path from 3, transfer(r7 = 10):
  r7 = r7 -&gt; r7 = 10.
- At 5, transfer(r6 += 1): r6 = r6 -&gt; r6 = (+ r6 1).
- At 2, join the two paths' contributions:
  join((+ r6 1), (+ r6 1)) = (+ r6 1) for r6;
  join(r7, 10) = (any r7 10) for r7.

Equal expressions stay unchanged; different expressions become ANY
alternatives. These summarize one iteration, without unrolling the loop.

Second phase:
-------------

The update r6 = (+ r6 1) says that each iteration adds 1 to r6.
Repeating this update n times gives r6_entry + n, a linear recurrence.

- At header 2, r6 = (+ r6 1) becomes (linear r6 1), meaning
  r6_entry + n, where n counts iterations from zero.
- At latch 6, substitute this recurrence into (+ r6 1):
  (+ (linear r6 1) 1) simplifies to (linear (+ r6 1) 1),
  meaning r6_entry + 1 + n.
- At both points, r7 retains (any r7 10): either its entry value
  or 10. ANY records alternatives, not numeric ranges or the path
  conditions selecting them. Unchanged variables retain their inputs.

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-33-bcba9bc53ac9@gmail.com
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Compute immediate dominators</title>
<updated>2026-10-09T20:29:13+00:00</updated>
<author>
<name>Eduard Zingerman</name>
<email>eddyz87@gmail.com</email>
</author>
<published>2026-10-09T10:47:41+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=6254fb69328963be95ff9b2760e879a9220ae6c3'/>
<id>6254fb69328963be95ff9b2760e879a9220ae6c3</id>
<content type='text'>
SCEV needs to find an exit condition that dominates a loop's backedge;
such conditions bound every loop iteration. Compute the immediate
dominator tree as a prerequisite for identifying such conditions.

Use the iterative reverse-postorder algorithm from:
"A Simple, Fast Dominance Algorithm" by Cooper et al.

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-23-bcba9bc53ac9@gmail.com
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
SCEV needs to find an exit condition that dominates a loop's backedge;
such conditions bound every loop iteration. Compute the immediate
dominator tree as a prerequisite for identifying such conditions.

Use the iterative reverse-postorder algorithm from:
"A Simple, Fast Dominance Algorithm" by Cooper et al.

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20261009-scev-minimal-rebase-v3-23-bcba9bc53ac9@gmail.com
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: crypto: Use AES-CBC and AES-ECB libraries</title>
<updated>2026-09-24T19:56:06+00:00</updated>
<author>
<name>Eric Biggers</name>
<email>ebiggers@kernel.org</email>
</author>
<published>2026-09-24T18:42:54+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=d5c101840af86a5b1451f8bd55cb8d76e1bfbb06'/>
<id>d5c101840af86a5b1451f8bd55cb8d76e1bfbb06</id>
<content type='text'>
BPF crypto was implemented using the lskcipher API, which doesn't seem
to be going anywhere.  lskcipher supports only ARC4 and block ciphers in
CBC and ECB mode, and only with unoptimized implementations.

Library APIs also have been found to be a much better approach, for a
variety of reasons, including reduced overhead, greater flexibility, and
having to be explicit about the crypto algorithms that are supported.

We can safely ignore the theoretical ARC4 and non-AES block cipher
support in BPF crypto as unused, which leaves AES-CBC and AES-ECB.
AES-CBC was stated to be needed for decrypting packets using a homebrew
UDP-based protocol
(https://lore.kernel.org/r/d1cdfc23-b336-49a9-8833-29f05b5b9fec@linux.dev/).
AES-ECB is used by the BPF self-tests, and it was stated to maybe be
used in the future for QUIC-LB
(https://lore.kernel.org/r/5f9c3aab-5339-463c-a86d-edac297e1e95@linux.dev/).

Those reasons don't make much sense either, especially AES-ECB which
isn't appropriate in new systems and should be dropped.  Regardless,
let's assume that both AES-CBC and AES-ECB need to be kept for now.

There are library APIs for both of these now, which are much easier to
use and more efficient.  Reimplement BPF crypto on top of them, greatly
simplifying the code.  As part of this, the bpf_crypto_type abstraction
layer is removed, as it's not useful.

This removes the only user of the lskcipher API, so follow-up patches
will be able to remove that code as well.

Signed-off-by: Eric Biggers &lt;ebiggers@kernel.org&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20260924184254.142720-1-ebiggers@kernel.org
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
BPF crypto was implemented using the lskcipher API, which doesn't seem
to be going anywhere.  lskcipher supports only ARC4 and block ciphers in
CBC and ECB mode, and only with unoptimized implementations.

Library APIs also have been found to be a much better approach, for a
variety of reasons, including reduced overhead, greater flexibility, and
having to be explicit about the crypto algorithms that are supported.

We can safely ignore the theoretical ARC4 and non-AES block cipher
support in BPF crypto as unused, which leaves AES-CBC and AES-ECB.
AES-CBC was stated to be needed for decrypting packets using a homebrew
UDP-based protocol
(https://lore.kernel.org/r/d1cdfc23-b336-49a9-8833-29f05b5b9fec@linux.dev/).
AES-ECB is used by the BPF self-tests, and it was stated to maybe be
used in the future for QUIC-LB
(https://lore.kernel.org/r/5f9c3aab-5339-463c-a86d-edac297e1e95@linux.dev/).

Those reasons don't make much sense either, especially AES-ECB which
isn't appropriate in new systems and should be dropped.  Regardless,
let's assume that both AES-CBC and AES-ECB need to be kept for now.

There are library APIs for both of these now, which are much easier to
use and more efficient.  Reimplement BPF crypto on top of them, greatly
simplifying the code.  As part of this, the bpf_crypto_type abstraction
layer is removed, as it's not useful.

This removes the only user of the lskcipher API, so follow-up patches
will be able to remove that code as well.

Signed-off-by: Eric Biggers &lt;ebiggers@kernel.org&gt;
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
Link: https://patch.msgid.link/20260924184254.142720-1-ebiggers@kernel.org
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf, keys: Add a bpf keyring for program signature validation</title>
<updated>2026-08-30T01:17:50+00:00</updated>
<author>
<name>Daniel Borkmann</name>
<email>daniel@iogearbox.net</email>
</author>
<published>2026-08-28T17:52:17+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=264d8fd2794fabe76a89abd5d4f5f8c1ed5fad85'/>
<id>264d8fd2794fabe76a89abd5d4f5f8c1ed5fad85</id>
<content type='text'>
BPF program signatures can currently be verified against one of the
system keyrings (builtin, secondary, platform) or against an arbitrary
user/session caller-supplied keyring named through keyring_id. There
is nothing in between: the system keyrings need a kernel rebuild or a
vouched-for enrollment to rotate a key, while a caller-supplied keyring
is fully controlled by the loader and therefore carries no trust on
its own (unless explicitly combined with BPF LSM to protect against
key tampering).

Add a dedicated bpf keyring to fill that gap, modelled after the
dm-verity keyring which was added in commit 033724b1c627 ("dm-verity:
add dm-verity keyring") and which can eventually be used also via
systemd [0] through the same enrollment method as in dm-verity's case.
It is selected with the new KEY_SPEC_BPF_KEYRING special key id and
gives an operator a place to enroll a BPF-only signing key at boot,
specifically scoped to BPF program loading and nothing else in the
kernel's trust hierarchy.

The id is reserved from the KEY_SPEC space so that the latter is not
linked into any process keyring, and lookup_user_key() resolves
KEY_SPEC_BPF_KEYRING constant instead of having to look it up via
/proc/keys first.

By default the keyring is sealed empty at init. Systems that want to
provision keys pass bpf.keyring_unsealed=1, which leaves the keyring
open for the initrd to add keys to. The keyring is only ever consulted
once it is both non-empty and restricted. An unrestricted keyring is
ignored.

Signed-off-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://github.com/systemd/systemd/pull/43549 [0]
Link: https://lore.kernel.org/r/20260828175227.1537793-2-daniel@iogearbox.net
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
BPF program signatures can currently be verified against one of the
system keyrings (builtin, secondary, platform) or against an arbitrary
user/session caller-supplied keyring named through keyring_id. There
is nothing in between: the system keyrings need a kernel rebuild or a
vouched-for enrollment to rotate a key, while a caller-supplied keyring
is fully controlled by the loader and therefore carries no trust on
its own (unless explicitly combined with BPF LSM to protect against
key tampering).

Add a dedicated bpf keyring to fill that gap, modelled after the
dm-verity keyring which was added in commit 033724b1c627 ("dm-verity:
add dm-verity keyring") and which can eventually be used also via
systemd [0] through the same enrollment method as in dm-verity's case.
It is selected with the new KEY_SPEC_BPF_KEYRING special key id and
gives an operator a place to enroll a BPF-only signing key at boot,
specifically scoped to BPF program loading and nothing else in the
kernel's trust hierarchy.

The id is reserved from the KEY_SPEC space so that the latter is not
linked into any process keyring, and lookup_user_key() resolves
KEY_SPEC_BPF_KEYRING constant instead of having to look it up via
/proc/keys first.

By default the keyring is sealed empty at init. Systems that want to
provision keys pass bpf.keyring_unsealed=1, which leaves the keyring
open for the initrd to add keys to. The keyring is only ever consulted
once it is both non-empty and restricted. An unrestricted keyring is
ignored.

Signed-off-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://github.com/systemd/systemd/pull/43549 [0]
Link: https://lore.kernel.org/r/20260828175227.1537793-2-daniel@iogearbox.net
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Add verifier diagnostics report helpers</title>
<updated>2026-08-15T18:11:16+00:00</updated>
<author>
<name>Kumar Kartikeya Dwivedi</name>
<email>memxor@gmail.com</email>
</author>
<published>2026-08-15T06:45:56+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=5ad746166341e3c07250ee09518d7e4ab5cfb966'/>
<id>5ad746166341e3c07250ee09518d7e4ab5cfb966</id>
<content type='text'>
Add the initial diagnostics renderer for verifier reports and wire it into
the BPF build. The helper emits the common failure header through the
verifier log.

Later patches add prose wrapping, reusable report sections, and source and
instruction context for category-specific diagnostics.

Gate the helpers on normal verifier log output from the start, so
BPF_LOG_STATS-only loads do not collect or render diagnostics.

Signed-off-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Link: https://patch.msgid.link/20260815064612.378577-2-memxor@gmail.com
Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Add the initial diagnostics renderer for verifier reports and wire it into
the BPF build. The helper emits the common failure header through the
verifier log.

Later patches add prose wrapping, reusable report sections, and source and
instruction context for category-specific diagnostics.

Gate the helpers on normal verifier log output from the start, so
BPF_LOG_STATS-only loads do not collect or render diagnostics.

Signed-off-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Link: https://patch.msgid.link/20260815064612.378577-2-memxor@gmail.com
Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: representation and basic operations on circular numbers</title>
<updated>2026-04-25T01:14:17+00:00</updated>
<author>
<name>Eduard Zingerman</name>
<email>eddyz87@gmail.com</email>
</author>
<published>2026-04-24T22:52:42+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=256f0071f9b61ae5028f749449fd3fdad015889d'/>
<id>256f0071f9b61ae5028f749449fd3fdad015889d</id>
<content type='text'>
This commit adds basic definitions for cnum32/cnum64.
This is a unified numeric range representation for signed and unsigned
domains. Inspired by an old post from Shung-Hsi Yu [1] and paper [2].
Operations correctness is verified using cbmc model checker,
tests source code can be found in a separate repo [3].

The cnum64_cnum32_intersect() function is notable, because it handled
several cases verifier.c:deduce_bounds_64_from_32() does not.
Given:
- a is a 64-bit range
- b is a 32-bit range
- t is a refined 64-bit range, such that ∀ v ∈ a, (u32)v ∈ b: v ∈ t.
cnum64_cnum32_intersect() makes the following deductions:

(A): 'b' is a sub-range of the first or the last 32-bit
     sub-range of 'a':

                                                         64-bit number axis ---&gt;

 N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
 ||------|---|=====|-------||----------|=====|-------||----------|=====|----|--||
         |   |&lt; b &gt;|                   |&lt; b &gt;|                   |&lt; b &gt;|    |
         |   |                                                         |    |
         |&lt;--+--------------------------- a ---------------------------+---&gt;|
             |                                                         |
             |&lt;-------------------------- t --------------------------&gt;|

(B) 'b' does not intersect with the first of the last 32-bit
    sub-range of 'a':

N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
||--|=====|----|----------||--|=====|---------------||--|=====|------------|--||
    |&lt; b &gt;|    |              |&lt; b &gt;|                   |&lt; b &gt;|            |
               |              |                               |            |
               |&lt;-------------+--------- a -------------------|-----------&gt;|
                              |                               |
                              |&lt;-------- t ------------------&gt;|

(C) 'b' crosses 0/U32_MAX boundary:

N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
||===|---------|------|===||===|----------------|===||===|---------|------|===||
 |b &gt;|         |      |&lt; b||b &gt;|                |&lt; b||b &gt;|         |      |&lt; b|
               |      |                                  |         |
               |&lt;-----+----------------- a --------------+--------&gt;|
                      |                                  |
                      |&lt;---------------- t -------------&gt;|

Current implementation of deduce_bounds_64_from_32() only handles
case (A).

[1] https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
[2] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
[3] https://github.com/eddyz87/cnum-verif/tree/master

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Link: https://lore.kernel.org/r/20260424-cnums-everywhere-rfc-v1-v3-1-ca434b39a486@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This commit adds basic definitions for cnum32/cnum64.
This is a unified numeric range representation for signed and unsigned
domains. Inspired by an old post from Shung-Hsi Yu [1] and paper [2].
Operations correctness is verified using cbmc model checker,
tests source code can be found in a separate repo [3].

The cnum64_cnum32_intersect() function is notable, because it handled
several cases verifier.c:deduce_bounds_64_from_32() does not.
Given:
- a is a 64-bit range
- b is a 32-bit range
- t is a refined 64-bit range, such that ∀ v ∈ a, (u32)v ∈ b: v ∈ t.
cnum64_cnum32_intersect() makes the following deductions:

(A): 'b' is a sub-range of the first or the last 32-bit
     sub-range of 'a':

                                                         64-bit number axis ---&gt;

 N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
 ||------|---|=====|-------||----------|=====|-------||----------|=====|----|--||
         |   |&lt; b &gt;|                   |&lt; b &gt;|                   |&lt; b &gt;|    |
         |   |                                                         |    |
         |&lt;--+--------------------------- a ---------------------------+---&gt;|
             |                                                         |
             |&lt;-------------------------- t --------------------------&gt;|

(B) 'b' does not intersect with the first of the last 32-bit
    sub-range of 'a':

N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
||--|=====|----|----------||--|=====|---------------||--|=====|------------|--||
    |&lt; b &gt;|    |              |&lt; b &gt;|                   |&lt; b &gt;|            |
               |              |                               |            |
               |&lt;-------------+--------- a -------------------|-----------&gt;|
                              |                               |
                              |&lt;-------- t ------------------&gt;|

(C) 'b' crosses 0/U32_MAX boundary:

N*2^32                   (N+1)*2^32                (N+2)*2^32                (N+3)*2^32
||===|---------|------|===||===|----------------|===||===|---------|------|===||
 |b &gt;|         |      |&lt; b||b &gt;|                |&lt; b||b &gt;|         |      |&lt; b|
               |      |                                  |         |
               |&lt;-----+----------------- a --------------+--------&gt;|
                      |                                  |
                      |&lt;---------------- t -------------&gt;|

Current implementation of deduce_bounds_64_from_32() only handles
case (A).

[1] https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
[2] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
[3] https://github.com/eddyz87/cnum-verif/tree/master

Signed-off-by: Eduard Zingerman &lt;eddyz87@gmail.com&gt;
Link: https://lore.kernel.org/r/20260424-cnums-everywhere-rfc-v1-v3-1-ca434b39a486@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Move BTF checking logic into check_btf.c</title>
<updated>2026-04-12T19:37:04+00:00</updated>
<author>
<name>Alexei Starovoitov</name>
<email>ast@kernel.org</email>
</author>
<published>2026-04-12T15:29:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=99a832a2b5b8a8ecc1a2bdd64017892caf4aa096'/>
<id>99a832a2b5b8a8ecc1a2bdd64017892caf4aa096</id>
<content type='text'>
BTF validation logic is independent from the main verifier.
Move it into check_btf.c

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-7-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
BTF validation logic is independent from the main verifier.
Move it into check_btf.c

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-7-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Move backtracking logic to backtrack.c</title>
<updated>2026-04-12T19:36:58+00:00</updated>
<author>
<name>Alexei Starovoitov</name>
<email>ast@kernel.org</email>
</author>
<published>2026-04-12T15:29:34+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=ed0b9710bd2efbe663d89728cd9c680c31c6a4e3'/>
<id>ed0b9710bd2efbe663d89728cd9c680c31c6a4e3</id>
<content type='text'>
Move precision propagation and backtracking logic to backtrack.c
to reduce verifier.c size.

No functional changes.

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-6-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Move precision propagation and backtracking logic to backtrack.c
to reduce verifier.c size.

No functional changes.

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-6-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>bpf: Move state equivalence logic to states.c</title>
<updated>2026-04-12T19:36:52+00:00</updated>
<author>
<name>Alexei Starovoitov</name>
<email>ast@kernel.org</email>
</author>
<published>2026-04-12T15:29:33+00:00</published>
<link rel='alternate' type='text/html' href='https://git.toradex.cn/cgit/linux-toradex.git/commit/?id=c82834a5a11f743f2926107d8f8150e80742b814'/>
<id>c82834a5a11f743f2926107d8f8150e80742b814</id>
<content type='text'>
verifier.c is huge. Move is_state_visited() to states.c,
so that all state equivalence logic is in one file.

Mechanical move. No functional changes.

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-5-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
verifier.c is huge. Move is_state_visited() to states.c,
so that all state equivalence logic is in one file.

Mechanical move. No functional changes.

Acked-by: Kumar Kartikeya Dwivedi &lt;memxor@gmail.com&gt;
Acked-by: Daniel Borkmann &lt;daniel@iogearbox.net&gt;
Link: https://lore.kernel.org/r/20260412152936.54262-5-alexei.starovoitov@gmail.com
Signed-off-by: Alexei Starovoitov &lt;ast@kernel.org&gt;
</pre>
</div>
</content>
</entry>
</feed>
