Interesting write-up. I get really, mixed reviews on all these analog designs from various EE's. So, what do you think about BitBabbler's analysis and design while you're at it?
EDIT: Now I know the name. Interesting to run into a person whose team independently invented a verifiable ASIC strategy very similar to my own of a year or so ago. I learned digital at a high-level, generalist way of thinking with no hands-on ability and definitely no analog. So, I have to work at that level. Started learning risk areas from insiders like this [1]. My initial strategy enumerated problem space to tackle it head on [2]. Yet, I switched gears to follow how provers work: combine untrusted EDA tools and main CPU's with traces produced for trusted, verification tools on inspectable CPU's. Similar to what I did for high-assurance, guard designs at protocol level without formal methods. I determined by maybe Jan2015 based on my Schneier.com posts that trusted ASIC's should be 0.35 micron or above because they're still visually inspectable. If ever funded, I'd modify VAMP CPU to be more like SAFE or CHERI to do the job. If too hard to do visual on, I'd start with a Forth or JOP-like processor before that. Even considered FM9001 & Piton haha. Also, replicating computation on diverse, fast CPU's from various vendors, fabs, and countries with optical communication & EMSEC isolation. The old, diverse, voter scheme I did pre-silicon for things like build systems.
Anyway, props on being ahead of me in implementation and more impressive design in general. Great work. That we converged on similar approach means it's probably worth me putting more effort into among the many ideas I'm juggling. I still gotta learn analog and hands-on formal methods, though, before I can do something like yours or provably solve the analog portion. (sighs) My gut has been telling me since I studied TEMPEST and RobertT's analog subversions that the solution will have strong analog component past diverse review of gates and such I was leaning on.
So, what do you think about BitBabbler's analysis and design while you're at it?
The problem with BitBabbler is that they have a lot of text but, as far as I can tell, no circuit diagrams and no real discussion of what they're doing. It may just be that their wall of text makes me go cross-eyed, but my snakeoil detector goes off whenever I start reading their web page. For example, the talk about sample-and-hold circuits as "analog shift registers" and worrying about quantization seems slightly unhinged (for one, if you need more resolution, just use a bigger sampling cap). Apologies to the BitBabbler people if they're on the up-and-up, but a page that talks about auditability and verifiability but doesn't show a schematic seems slightly dishonest.
(Sorry... rant mode off.)
Thanks for the kind words regarding verifiable ASICs! You are absolutely right that there's a ton of complexity to worry about here. But I sincerely hope that the world makes more headway on this problem, so I'm really glad you're thinking about it.
http://www.bitbabbler.org/how.html
EDIT: Now I know the name. Interesting to run into a person whose team independently invented a verifiable ASIC strategy very similar to my own of a year or so ago. I learned digital at a high-level, generalist way of thinking with no hands-on ability and definitely no analog. So, I have to work at that level. Started learning risk areas from insiders like this [1]. My initial strategy enumerated problem space to tackle it head on [2]. Yet, I switched gears to follow how provers work: combine untrusted EDA tools and main CPU's with traces produced for trusted, verification tools on inspectable CPU's. Similar to what I did for high-assurance, guard designs at protocol level without formal methods. I determined by maybe Jan2015 based on my Schneier.com posts that trusted ASIC's should be 0.35 micron or above because they're still visually inspectable. If ever funded, I'd modify VAMP CPU to be more like SAFE or CHERI to do the job. If too hard to do visual on, I'd start with a Forth or JOP-like processor before that. Even considered FM9001 & Piton haha. Also, replicating computation on diverse, fast CPU's from various vendors, fabs, and countries with optical communication & EMSEC isolation. The old, diverse, voter scheme I did pre-silicon for things like build systems.
Anyway, props on being ahead of me in implementation and more impressive design in general. Great work. That we converged on similar approach means it's probably worth me putting more effort into among the many ideas I'm juggling. I still gotta learn analog and hands-on formal methods, though, before I can do something like yours or provably solve the analog portion. (sighs) My gut has been telling me since I studied TEMPEST and RobertT's analog subversions that the solution will have strong analog component past diverse review of gates and such I was leaning on.
[1] https://www.schneier.com/blog/archives/2013/09/surreptitious...
[2] https://news.ycombinator.com/item?id=10468624