News for hackers. Stuff that matters.
Re:Formal Verification Creates Hacker-Proof Code by nickpsecurity on Friday October 21, 2016 @07:16PM (#12765733)
It's always been there. The messiness & limitations of analog were actually main the reasons for digital being invented in the first place. Then the digital stuff had issues but way easier to surmount with formal methods. Or just computationally like heuristic placement of parts. Each problem that was found could be dealt with using known algorithms or verification techniques. There's been many correct-by-construction methods to building stuff. So, we just apply that without the weird, over-complicated additions that happened largely for marketing reasons. The result is a highly-correct, reference implementation there for verification or checking the optimized ones.

Now, the analog and RF portions are The Devil. These will be a (censored) to get correct with automated means. Already are with manual methods. There's been some progress in synthesizing and verifying them. Still mostly ad-hoc, manual work. Best bet is analog portions... much as one can use... happen with simple components on as old a process node as you can use. Less design rules, less weird physics, more reliability due to maturity of processes, and more synthesis results. Either whole thing is done on old nodes or we can pull a Tekmos doing old (eg 350nm) for analog with new (eg 90nm) for digital part with careful integration.

EDIT: To address other commenter, put it behind EMSEC shielding to address that. The analog components can also be designed for fault-tolerance against things like cosmic rays or voting configuration used to correct errors.

There are no comments on this comment yet.