netdev - Re: [PATCH net-next v10 1/4] rust: core abstractions for network PHY drivers

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <b2cba04e-0201-48b7-a34f-81dbd7b799ff@lunn.ch>
Date: Thu, 14 Dec 2023 10:26:36 +0100
From: Andrew Lunn <andrew@...n.ch>
To: Benno Lossin <benno.lossin@...ton.me>
Cc: Boqun Feng <boqun.feng@...il.com>,
	FUJITA Tomonori <fujita.tomonori@...il.com>, alice@...l.io,
	netdev@...r.kernel.org, rust-for-linux@...r.kernel.org,
	tmgross@...ch.edu, miguel.ojeda.sandonis@...il.com,
	wedsonaf@...il.com, aliceryhl@...gle.com
Subject: Re: [PATCH net-next v10 1/4] rust: core abstractions for network PHY
 drivers

On Wed, Dec 13, 2023 at 11:40:26PM +0000, Benno Lossin wrote:
> On 12/13/23 22:48, Andrew Lunn wrote:
> >> Well, a safety comment is a basic part of Rust, which identifies the
> >> safe/unsafe boundary (i.e. where the code could go wrong in memory
> >> safety) and without that, the code will be just using Rust syntax and
> >> grammar. Honestly, if one doesn't try hard to identify the safe/unsafe
> >> boundaries, why do they try to use Rust? Unsafe Rust is harder to write
> >> than C, and safe Rust is pointless without a clear safe/unsafe boundary.
> >> Plus the syntax is not liked by anyone last time I heard ;-)
> > 
> > Maybe comments are the wrong format for this? Maybe it should be a
> > formal language? It could then be compiled into an executable form and
> > tested? It won't show it is complete, but it would at least show it is
> > correct/incorrect description of the assumptions. For normal builds it
> > would not be included in the final binary, but maybe debug or formal
> > verification builds it would be included?
> 
> That is an interesting suggestion, do you have any specific tools in
> mind?

Sorry, no. I've no experience in this field at all. But given the
discussions this patch has caused, simply a list of C or Rust
expressions which evaluate to True when an assumption is correct would
be a good start.

We have said that we assume the phydev->lock is held. That is easy to
express in code. We have said that phydev->mdio must be set, which is
again easy to express. phydev->mdio.addr must be in the range
0..PHY_MAX_ADDR, etc.

You probably cannot express all the safety requirements this way, but
the set you can describe should be easy to understand and also
unambiguous, since it is code. The rest still can be as comments.  It
would be easy to compile this code and insert it before the function
on a verification build. Its only runtime checking, but its more
functional than comments which the compiler just throws away. And
maybe subsystems like this which are pretty much always slow path
might even leave them enabled all the time, to act as a set of
assert()s, which you sometimes see in code bases.

	Andrew