|
![](/i/fill.gif) |
On 6/6/2011 15:13, clipka wrote:
> Ah yes - a formal proof... pretty useful if your intention is to make sure a
> security-critical system never fails due to unforeseen errors.
That is the intention.
> As for making sure that a system is secure against /malicious intent/, I
> believe it's pretty useless.
No, it's very good at that.
> ... on its /official/ interface, i.e. the I2C bus data lines.
Naturally. All you're saying is that a formal system won't break as long as
the underlying system matches the formalism.
It's *much* more difficult to mount an attack against a smart card when
you're not physically in possession of the smart card than when you are.
Plus, again, the attacks on the smart card aren't the same category as
malware. With DRM, the card (or console or whatever) has to be able to
perform its operations while hiding its results from observers. With
malware, the system doesn't want to perform the operations at all.
The system relies on programs to obey the rules that the system enforces,
just like your operating system relies on the hardware doing what the
hardware says it does.
> Say you will - I think a formal analysis can never foresee /all/ possible
> attack vectors a system might exhibit.
It depends on the kind of attack you're trying to prevent. It's easy to show
that formal analysis can foresee you never running off the end of an array
to access memory belonging to another process. How much malware have you
seen that takes advantages of flaws in the CPU mask? Formal analysis can
foresee all possible attack vectors for particular attacks, assuming the
mathematical system is isomorphic with the physical system. Of course if
you're trying to hide information in one program from being observed by
another, you have to take care that things not accounted for in the
formalism (such as the timing) don't happen. But the things accounted for by
the formalism can be shown not to happen, as long as the hardware (et al)
obeys the same rules as the formalism.
In other words, it becomes far easier to check you're right, because you've
written a very few number of rules that you have to manually check are
correct, and the computer deduces from them that the top-level properties
you want to hold do indeed hold.
And there have been formally-verified chip designs as well, where the
assembly language was expressed in math and they proved that the chip mask
made the chip follow the spec. (To some extent, I assume. I would imagine it
would be difficult to prove that, for example, what you etched is what you
thought you etched.)
--
Darren New, San Diego CA, USA (PST)
"Coding without comments is like
driving without turn signals."
Post a reply to this message
|
![](/i/fill.gif) |