ioctl() forever? [LWN.net]

ioctl() forever?

Posted Jun 9, 2022 15:11 UTC (Thu) by ejr (subscriber, #51652)
In reply to: ioctl() forever? by roc
Parent article: ioctl() forever?

To paraphrase the bard, "That way [formal methods] lie; let me shun that."

to post comments

ioctl() forever?

Posted Jun 12, 2022 0:16 UTC (Sun) by developer122 (guest, #152928) [Link] (7 responses)

Such is the pervading wisdom in software.

It was yesterday I was commented that modern security practice is to layer incomplete speedbumps one by one and call it "defense in depth." This was in response to new bypass of the M1's hardware pointer checking, a "last line of defense."

None of these half-baked measures qualify as defense in depth. Anyone who calls it that is kidding themselves. They're deployed one by one with large time spans inbetween, reactively to whatever attackers currently favor. It should come as no surprise that attackers have no problem paying a low continual cost to work around each new measure, in return for continued ability to exploit hosts.

Meanwhile, we plaster over the undefined behavior that makes C/C++ static analysis impractical. We don't even talk about how CPUs work. We continue to ignore that actual exploit *theory* exists, like the Weird Machine whose wikipedia page starts: "Exploits exist empirically, but were not studied from a theoretical perspective prior to the emergence of the framework of weird machines." This makes it impossible to analyze systems holistically, and to find and shut out entire classes of exploits.

Civil engineering eventually got past "I think we can cut a small hole in this wall" and reached "lets calculate the loads and strains." Electrical engineering stopped electrocuting frogs and developed Maxwell's laws. Right now computing is still far behind all others and until formal methods and theory take over, we won't ever make statements like "this bridge will stand for 100 years."

ioctl() forever?

Posted Jun 12, 2022 1:15 UTC (Sun) by Cyberax (✭ supporter ✭, #52523) [Link] (6 responses)

> Electrical engineering stopped electrocuting frogs and developed Maxwell's laws.

Open the NEC and look for any mentions of Maxwell's equations. If anything, modern safety engineering is built on installing as many "speedbumps" as possible, rather than on making everything perfectly safe.

ioctl() forever?

Posted Jun 12, 2022 9:01 UTC (Sun) by farnz (subscriber, #17727) [Link] (5 responses)

The NEC (and its international equivalents) are guides to safe installation, not to electrical engineering. It says that if you purchase products that have been engineered to a suitable standard, and then install them following this guide, you will be safe enough.

The components you install when you buy the things that the NEC requires are engineered with things like Maxwell's laws as guidance - a GFCI or an AFCI or an ELCB or an overcurrent breaker, or even a simple switch is not just empirically designed to work as specified, but rather designed around the known laws of physics and then tested against the specification.

It's just that we need the NEC rules because the possible range of components is not as wide as we'd like - and thus we need to allow for known physical issues when we install. For example, we need overcurrent breakers because wires have resistance and thus heat up when carrying current; a significant chunk of the NEC is describing the different ways you can install wires that meet a given standard, then place a breaker on the source end so that the wire cannot heat up enough to start a fire.

ioctl() forever?

Posted Jun 12, 2022 15:01 UTC (Sun) by ejr (subscriber, #51652) [Link] (4 responses)

The main problem is that the market for electrical engineers actually *designing* these things is relatively static or slowly growing. Meanwhile, companies are absolutely desperate to fill programming seats.

And if it ain't Python or Matlab/Octave, many students don't know it until maybe their third year. Maybe. If type checking is not mentally established, the core of current formal methods that include interactive proofs is going nowhere. (For the audience: Making a program compile without type errors *is* working with an interactive proof system called the compiler. The correct program is a proof of its being well-typed given the language's rules / axioms.)

I also suspect you underestimate how often "throw it at the wall and see if it sticks" applies even in engineering fields. Or more appropriately "this worked for something kinda similar, so it'll work here."

I recently learned of a wonderful text that can illustrate the kind of knowledge needed on the practical hardware side: D. M. Russinoff, Formal Verification of Floating-Point Hardware Design, https://doi.org/10.1007/978-3-030-87181-9_3 . It *appears* to be available gratis; I don't think I was redirected through an institutional subscription.

Software potentially could be simpler in some areas, but the OS/device level requires a similar level of skill in finding the right model. That's a polite way of saying the kind of infinite bike-shedding that was happening with btrfs. If some research group can hit it out of the park like the formalization of RISC-V, sure, but people with product-like deadlines don't have that time. (I've been on both sides.)

ioctl() forever?

Posted Jun 12, 2022 15:37 UTC (Sun) by mpr22 (subscriber, #60784) [Link] (2 responses)

You were in fact directed there by an institutional subscription :(

For me, that link goes to a website run by Springer Nature, where I am informed that, as a private individual in the United Kingdom of Great Britain and Northern Ireland, I would have to pay £19.95 for a PDF of the Logical Operations chapter (pp 35-44) of ISBN 978-3-030-87181-9, £95.50 for the whole of ISBN 978-3-030-87181-9 as an eBook, or £119.99 for the whole of ISBN 978-3-030-87181-9 as a physical hardcover book (all prices inclusive of applicable VAT).

ioctl() forever?

Posted Jun 13, 2022 21:57 UTC (Mon) by ejr (subscriber, #51652) [Link]

AUGH. Drat. Sorry! I was hoping, and I didn't see how I was already logged in. There is no RTL in the book at all but rather proofs based around integers. That's kinda how I think of circuits, so I like it.

ioctl() forever?

Posted Jun 14, 2022 12:54 UTC (Tue) by paulj (subscriber, #341) [Link]

It is archived by sci-hub.se, depending on what you think of that kind of thing.

ioctl() forever?

Posted Jun 12, 2022 16:06 UTC (Sun) by farnz (subscriber, #17727) [Link]

And underlying that is that electrical safety is a mature and well-understood field. The physics involved in a GFCI or an overcurrent breaker have been well-understood since the 19th century, and the physics required for an AFCI were fully settled before World War I in 1914. There's nothing in any NEC-compliant installation that a good physicist from 1920 couldn't fully understand and explain - although they'd be amazed by the manufacturing techniques involved (and would be seriously shocked by the IC in an AFCI, even though they could explain the physical principles that underpin its operation).

In contrast, logic design (both software and hardware) is a rapidly evolving field even today - Rust's type system is based atop affine logic from the 1970s, and there's mathematics I'm aware of that's probably relevant to programming language design that was only formulated rigorously in the last 20 years, and where there's active leading-edge research trying to determine if it's useful, and if so, how.

I'd also agree on the "throw it at the wall and see if it sticks" thing - the only time, IME, that engineers actually seriously bother with the rigorous analysis that's possible for something like a GFCI is when you're cost-optimizing it. Otherwise, it's considered too much work, when you can take a design that's probably overkill but meets requirements and ship it.