From nobody Thu Sep 12 06:29:38 2024
X-Original-To: freebsd-hackers@mlmmj.nyi.freebsd.org
Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1])
	by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4X46x95FlDz5TyKw
	for <freebsd-hackers@mlmmj.nyi.freebsd.org>; Thu, 12 Sep 2024 06:29:49 +0000 (UTC)
	(envelope-from gavin@gavinhoward.com)
Received: from mail-4317.proton.ch (mail-4317.proton.ch [185.70.43.17])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)
	 key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256
	 client-signature RSA-PSS (4096 bits) client-digest SHA256)
	(Client CN "protonmail.com", Issuer "R11" (verified OK))
	by mx1.freebsd.org (Postfix) with ESMTPS id 4X46x73pnWz4Lm6
	for <freebsd-hackers@FreeBSD.org>; Thu, 12 Sep 2024 06:29:47 +0000 (UTC)
	(envelope-from gavin@gavinhoward.com)
Authentication-Results: mx1.freebsd.org;
	dkim=pass header.d=gavinhoward.com header.s=protonmail3 header.b=Hy0rupHV;
	dmarc=pass (policy=quarantine) header.from=gavinhoward.com;
	spf=pass (mx1.freebsd.org: domain of gavin@gavinhoward.com designates 185.70.43.17 as permitted sender) smtp.mailfrom=gavin@gavinhoward.com
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gavinhoward.com;
	s=protonmail3; t=1726122582; x=1726381782;
	bh=QAmKSSQaggjol4eYGFjGxy/LBpMgE7fM0GWTXEcHwJE=;
	h=Date:To:From:Subject:Message-ID:In-Reply-To:References:
	 Feedback-ID:From:To:Cc:Date:Subject:Reply-To:Feedback-ID:
	 Message-ID:BIMI-Selector;
	b=Hy0rupHVYBcIvYUlU9w7JRe70p39vmqfmyOAzxFVuFh2HyxGktF8IwUPPbf9nCWSa
	 q27aemlnCM4pRXWTJjYQu3J0CPoECBKn0Pg5WRPV4RAEBsxCxXtI/l+rbjGw2ctr8z
	 EesxeQKqyciCezU8TaRS7d2VrFL3U/eRA1jnefC4s747lZsux9ii65qpZ/nAdILen4
	 XNODJrRrtuQHfU0eZgf3zAl75O1XOrSFQ8BDExuyjkr1dkZq4zBn5X73YsD89lnCfN
	 6Nsm38lCmvq5PRF3S1pXnC4tV+YUxQjxrFn4zfFdpj5tjuwV76EAEToUwEc3My/L7k
	 UHRFoXp+wpmXQ==
Date: Thu, 12 Sep 2024 06:29:38 +0000
To: "freebsd-hackers@FreeBSD.org" <freebsd-hackers@FreeBSD.org>
From: "Gavin D. Howard" <gavin@gavinhoward.com>
Subject: Re: BPF64: proposal of platform-independent hardware-friendly backwards-compatible eBPF alternative
Message-ID: <f9KxenmdwQZ8oQrcH6ePy30goR2nOPYCULfkQnFaugR0mFpoL_THbqWwt4Jkt4FKpe03xXULUwRCSc8rUdIsnCSeG2X03iSpfNczBy-vks8=@gavinhoward.com>
In-Reply-To: <20240910181711.5d324ac5@nuclight.lan>
References: <20240910040544.125245ad@nuclight.lan> <wLzD36W8VSXSlBByVmK745ezszNVGM-hfWOobdrCb1vmx9snihwW_gBgeAlvtKWL55fnAZgr9G5ztIO3UjD3Wou3-YPxmLkMp9AFuGHwXsA=@gavinhoward.com> <20240910181711.5d324ac5@nuclight.lan>
Feedback-ID: 18790518:user:proton
X-Pm-Message-ID: 8d0760b21a122fadbb2d01b393e1cdf20d5127c6
List-Id: Technical discussions relating to FreeBSD <freebsd-hackers.freebsd.org>
List-Archive: https://lists.freebsd.org/archives/freebsd-hackers
List-Help: <mailto:freebsd-hackers+help@freebsd.org>
List-Post: <mailto:freebsd-hackers@freebsd.org>
List-Subscribe: <mailto:freebsd-hackers+subscribe@freebsd.org>
List-Unsubscribe: <mailto:freebsd-hackers+unsubscribe@freebsd.org>
Sender: owner-freebsd-hackers@FreeBSD.org
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spamd-Bar: ----
X-Spamd-Result: default: False [-4.20 / 15.00];
	NEURAL_HAM_LONG(-1.00)[-1.000];
	NEURAL_HAM_MEDIUM(-1.00)[-1.000];
	NEURAL_HAM_SHORT(-1.00)[-1.000];
	DMARC_POLICY_ALLOW(-0.50)[gavinhoward.com,quarantine];
	R_SPF_ALLOW(-0.20)[+ip4:185.70.43.0/24];
	R_DKIM_ALLOW(-0.20)[gavinhoward.com:s=protonmail3];
	RWL_MAILSPIKE_VERYGOOD(-0.20)[185.70.43.17:from];
	MIME_GOOD(-0.10)[text/plain];
	FREEFALL_USER(0.00)[gavin];
	ASN(0.00)[asn:62371, ipnet:185.70.43.0/24, country:CH];
	MIME_TRACE(0.00)[0:+];
	FROM_HAS_DN(0.00)[];
	MISSING_XM_UA(0.00)[];
	TO_MATCH_ENVRCPT_ALL(0.00)[];
	RCPT_COUNT_ONE(0.00)[1];
	TO_DN_EQ_ADDR_ALL(0.00)[];
	MLMMJ_DEST(0.00)[freebsd-hackers@FreeBSD.org];
	FROM_EQ_ENVFROM(0.00)[];
	MID_RHS_MATCH_FROM(0.00)[];
	RCVD_COUNT_ZERO(0.00)[0];
	ARC_NA(0.00)[];
	DKIM_TRACE(0.00)[gavinhoward.com:+]
X-Rspamd-Queue-Id: 4X46x73pnWz4Lm6

> > If I understand Turing-completeness correctly, the "no backward jumps
> > but allow recursion and quit on stack overflow" is exactly equivalent
> > to having non-infinite loops.
>
> Sure, but then look at practical usefulness: suppose you have stack of
> 32 frames (current limit of eBPF and BPF64). Then you can have only 31
> iterations on a loop, loosing ability to call more functions from loop
> body.

That is true.

However, I wonder if everyone is going at this the wrong way. More
specifically, I wonder if we are targeting the entirely wrong level.
Maybe verifying bytecode or some other low-level code form is just too
hard. What if it were easier just to provide a higher level language
that had enough restrictions to be just barely not Turing-complete.

To test that idea, I did a quick experiment.

I have been working on a language called Yao for the past three years.
One feature I planned for the future was the ability to restrict what
packages and keywords are available at compile time. I had already
put in the plumbing, but I just hadn't implemented it.

But I decided to quickly implement it as an experiment.

First, I needed a stack limit:

https://git.yzena.com/Yzena/Yc/commit/99c822bf7b

Now, you can run this:

```
$ ./release/yc yao --max-stack-depth=3D32 <script>
```

and you get the same max stack depth as eBPF.

Next, restricting keywords. One unique thing about Yao is that *every*
keyword is imported like you would import functions, even standard ones
like `if` and `while`. This means that if a keyword is not allowed, I
can just skip importing it, and it's like it doesn't even exist.

So I built a way to skip importing the `while` keyword and any other
keyword that would make the language Turing-complete. Crucially, though,
it still includes a `foreach` loop, so backwards jumps are still
possible.

A script with a `while` loop is `tools/rig_slam.yao` in the same repo.
If you run:

```
$ make # This bootstraps the repo.
$ ./release/yc yao tools/rig_slam.yao
```

you will get a panic when it tries to parse the `while` loop because I
haven't implemented the parsing:

```
Panic: Unimplemented
    Source:    /home/gavin/Yzena/Code/yc-git/yc/src/yao/keywords.c:2310
    Function:  yao_parse_while()
```

But if you run this:

```
$ ./release/yc yao --max-stack-depth=3D32 --lang-mode=3Diterative \
  tools/rig_slam.yao
```

you get a compile error, and it doesn't even try to parse the `while`:

```
yc: tools/rig_slam.yao[145:2]
    Parse error: Incomplete variable declaration for name: while

yc: tools/rig_slam.yao[145:8]
    Invalid token: Expected semicolon (';')
```

(You also get a different panic after that because Yao has bugs.)

Anyway, essentially, the "iterative" language mode with a max stack
depth makes Yao non-Turing-complete, but with a way to loop.

You can try that with `tools/format.yao`, which has a `foreach` loop:

```
$ ./release/yc yao --max-stack-depth=3D32 --lang-mode=3Diterative \
  tools/format.yao
```

and it still works.

I'm not saying Yao as an eBPF replacement is a good idea; it's not. But
I think this demonstrates that a simple high-level language with a
simple compiler and a simple VM might be a viable method of implementing
an eBPF-like thing without a complex verifier.

Yes, the compiler and VM would need to be in the kernel, but that might
already be the case with the JIT in Linux.

Anyway, my point is that before FreeBSD accepts BPF64, it might be a
good idea to sit down and consider all of the options, brainstorm ideas
together, and make an excellent design.

And it could very well be that BPF64 *is* the best design! I don't know;
I'm not a kernel guy, nor am I an expert compiler guy.

> > * But the analysis pass(es) must still live in the kernel.
> > * There would need to be tutorials or some docs on how to write
> > whatever language so that backwards jumps are avoided.
>
> So BPF64 took simplicity pass: while you have tutorials etc. it's still
> very hard to write (non-toy) code that passes verifier. I think a
> language where you do not need backward jumps but have usable
> constructs (so you just can't write bad code), even BAW, is a better
> way to go than try to train people to fight with unnecessary Cerber.

Yes, I think you are right on this, which IMO just points to a
high-level language. Such a language can have whatever constructs are
safe, but by its very nature, it will be restricted such that dangerous
code is impossible.

It would also be easier to write code that passes the "verifier" if the
verifier is actually the compiler.

Anyway, I hope I don't sound too critical; I don't have the chops to
judge BPF64. Plus, I can tell you put in a lot of work.

Gavin Howard