[bitc-dev] [Fwd: Re: Bitc]

[Jonathan S. Shapiro]

On Mon, 2006-08-07 at 01:00 +0200, Guillaume FORTAINE wrote:

>What is a B3-secure architecture ? :
> 
> http://www.erights.org/history/index.html

This is a reference to the B-3 security "level" defined by the Orange
Book, also known as the Trusted Computer System Evaluation Criteria
(DOD-5200.28-STD). You will sometimes see this document referred to as
"TCSEC".

>Maybe it's time to move from industrial to military grade in
>open-source community :-).

:-)

Seriously: God I hope not, because most of that stuff was completely
unusable in practice. What we need is something usable that works. This
is much harder than rebuilding B3.

> What are you suggestions to enhance BitC in describing sophisticated 
> invariants ( some links, info to have a start point).

>From a developer perspective, the best existing technology for this is
probably ACL2. There are provers that use theoretically more advanced
technologies, but none of these have good integration with the
programming environment. ACL2 is the clear leader from the perspective
of *programmers* (as opposed to verification researchers).

The problem with ACL2 is that it's based on a language that does not
provide either mutation or representation, and has no static type
system.

So, I would like to achieve two things:

1. An ACL2-like environment with a production-capable programming
language, and

2. Some "intermediate" steps. Full verification is a big thing to jump
in to. Intermediate techniques like model checking are very powerful and
have a smaller cost of entry for the programmer. There is no reason why
*all* of these techniques cannot be integrated into a single
environment.


shap