[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Henry Baker]

At 10:49 PM 3/21/2016, dj at deadhat.com wrote:
>This is exactly the same as having a tool that would verify that compiled machine code is formally equivalent to the C that the compiler translated it from.
>
>This is because in digital logic, no one trusts the synthesizer, whereas in software, only the security people seem to mistrust the C compiler.

https://web.stanford.edu/class/ee380/Abstracts/150304.html

Stanford EE Computer Systems Colloquium
4:15PM, Wednesday, March 4, 2015
NEC Auditorium, Gates Computer Science Building Room B3
http://ee380.stanford.edu

Dynamic Code Optimization and the NVIDIA Denver Processor

Nathan Tuck NVIDIA

About the talk:

NVIDIA's first 64-bit ARM processor, code-named Denver, leverages a host of new technologies to enable high-performance mobile computing.  Implemented in a 28-nm process, the Denver CPU can attain clock speeds of up to 2.5 GHz.  This talk will outline the Denver architecture and describe some of its technological innovations.  In particular this talk will discuss some of the motivations and advantages of dynamic code optimization.

Slides:

There not downloadable slides for this presentation available at this time.

Videos:

View Video on YouTube.

http://youtu.be/oEuXA0_9feM

About the speaker:

Nathan Tuck has been a member of the DCO and CPU architecture teams at NVIDIA since 2009.

Nathan has spent his professional career walking a crooked line between hardware and software.  As an engineer, he is most interested in working on systems problems.  Professionally, he is most interested in dynamic environments where he can make a large difference.

Contact information:

Nathan Tuck
NVIDIA
-------
FYI -- "DCO": Yet more lovely places for malware to hide.  The executing code is "translated" into a microcode buffer, but who gets to be in charge of said translation?

"Those who cast the votes decide nothing.  Those who count the votes decide everything."  -- Josef Stalin

I believe that these DCO processors have already been picked up for widespread use in automobiles, including self-driving cars.

What, me worry?
---------
Above is a message I sent almost a year ago about nVidia's new "DCO" mechanism, where the standard computer op codes are merely a gentle hint/suggestion about what the CPU should actually do.  Behind the scenes, "DCO" can re-interpret your *hardware op code* to do anything it damn well pleases.  This is the opcode equivalent of *memory maps*, which merely provide gentle hints/suggestions about where to fetch instructions.

See the Youtube video link above for more details.