Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.arch.embedded > #30636

Re: (Semi-) formal methods

Show all headers | View raw

On 5/15/2021 4:02 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote:
>> Understood.  Tools fit the application domains for which they were designed.
>>
>> How did *adoption* of the tool come to pass?  Was it "mandated" by corporate
>> policy?  Something <someone> stumbled on, played with and then "pitched"
>> to management/peers?  Mandated by your industry?  etc.
>>
>> [Just because a tool "makes sense" -- logically or economically -- doesn't
>> mean it will be adopted, much less *embraced*!]
> 
> We're a university research lab.  We developed the tool in response to two
> trends:
> 
> - growing complexity of systems and the increasing prevalence of bugs in
> implementation (for example in memory coherency subsystems).
> 
> - proposing security extensions to architectures and wanting to be able to
> show that what we've proposed doesn't have any loopholes in it.  It provides
> confidence to us and to people adopting the technology that the technology
> is robust, and there won't be problems once silicon is deployed and
> impossible to fix later.

OK.  Both make sense.  And, both are hard (if not impossible) to "fix"
at layers *above* the hardware.

The next, most practical, question is:  how do you encourage its adoption?
Publishing papers is what professors/grad students "do".  That's
different from actually getting folks to *use* something that you've
developed/written about.

(a casual examination of the amount of "stuff" that has come out of
academia and "gone nowhere" -- despite some value! -- should make
this evident)

> (that's not to say there won't be entirely new classes of attacks coming out
> of left-field in the way that Spectre surprised a lot of people, but are at
> least trying to reason about the attacks we know about)
> 
> Because the costs of respinning are so high, chip design is all about
> verification.  Doing it in a formal sense is a step up from hand-writing or
> randomly-generating tests.  I don't think the industry needs convincing that
> it's a good idea in abstract - it's mainly making the benefits outweigh the
> costs.  A lot of the work (eg in the RISC-V community) is about bringing
> down those costs.

Understood.  In the past, I've had to rely on "good eyes" to spot problems
in designs.  Folks tend to only test how they *think* the design SHOULD
perform.  So, they often omit checking for things that they don't imagine
it (mis?)doing.

<do something; witness crash>
"What did you just do?"
"This..."
"You're not supposed to do that!"
"Then why did you/it LET ME?  Did I break some *law*???"

[Thankfully, I have a nack for identifying MY "assumptions" and the
liabilities that they bring to a design]

A suitably aggressive tool can avoid this bias and just hammer at every
nit it can algorithmically deduce/exploit.

A colleague designed a video scaler for a printer.  When I started poking at
it with real numbers, I discovered cases where the PHYSICAL image size
produced on a B-size page was actually SMALLER than that produced on an
A-size page (presumably, you'd print on larger paper to get a larger image!).

Ooops!

Given the number of variations in how the interface could be configured,
he'd never have been able to exhaustively test all cases.  So, my observation
was just serendipitous.

OTOH, *seeing* what I'd uncovered gave him cause to look more carefully
at his implementation *before* sending it off to fab (which would have cost
money AND calendar time -- leading to a delayed market introduction).

Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

(Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-11 18:25 -0700
  Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-13 15:25 +0100
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 11:57 -0700
      Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-14 10:43 +0100
        Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 12:37 -0700
          Re: (Semi-) formal methods HT-Lab <hans64@htminuslab.com> - 2021-05-15 08:44 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:48 -0700
          Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-15 12:02 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 15:07 -0700
  Re: (Semi-) formal methods Dave Nadler <drn@nadler.com> - 2021-05-13 19:32 -0400
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 16:57 -0700
    Re: (Semi-) formal methods Paul Rubin <no.email@nospam.invalid> - 2021-05-14 12:22 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:55 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:52 -0700
    Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 18:14 +1000
      Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:10 -0700
        Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 20:54 +1000
          Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 12:26 -0700
            Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-16 11:41 +1000
              Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-16 00:35 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 12:03 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-01 22:23 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 22:39 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-02 09:01 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-03 11:54 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-03 01:56 -0700
  Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 14:15 +1000

csiph-web