The Coq mailing list

[Sam Kuper <sampablokuper AT posteo.net>]

On Tue, Jan 11, 2022 at 01:50:16PM +1100, Jeremy Dawson wrote:
> On 11/1/22 12:49, Robert Solovay wrote:
>> What, precisely,  does TCB mean in these letters?
>
> I presume, trusted computing base.

Almost certainly.

https://en.wikipedia.org/wiki/Trusted_computing_base


> The bit that has got to work right.

The TCB has been variously defined.

I tend to think of it in the following terms, inspired by e.g. Joanna
Rutkowska, but others think of it differently:

    The key point in understanding what a TCB is, is to make a
    distinction between "trustworthy" and "trusted".

    -   "Trustworthy" hardware or software is formally verified to be
        correct and secure (for appropriate definitions of those
        terms...).  As such, no leap of faith needs to be made in order
        for a person to trust that it will perform accordingly.

        Shrinking the *trustworthy* computing base may be sensible from
        an efficiency perspective, but is not necessary from a security
        or correctness perspective.

        The TCB is not *trustworthy*.

    -   "Trusted" hardware/software - the TCB - by contrast, is not
        formally verified to be correct.  As such, a leap of faith is
        required in order for a person to trust that it will perform
        securely and correctly.

        To the extent that a person trusts the TCB, this is by necessity
        (e.g. not having access to a more trustworthy computing device)
        or by ignorance, not by justification.

        As such, eliminating (or at least shrinking) the TCB is
        desirable from a security and correctness perspective.  The
        smaller it is, the fewer places for incompetent or malicious
        properties to hide within it - and the lower the risk to its
        users.

Projects like Sandsifter (an x86 processor fuzzer) illustrate just how
huge and hellish the TCB can be in today's computers.


> You design your software to make this as small and simple as possible.

Yes, and preferably your hardware too, cf. Talia's question.

Sam

-- 
A: When it messes up the order in which people normally read text.
Q: When is top-posting a bad thing?

()  ASCII ribbon campaign. Please avoid HTML emails & proprietary
/\  file formats. (Why? See e.g. https://v.gd/jrmGbS ). Thank you.