[C-safe-secure-studygroup] C-safe-secure-studygroup Digest, Vol 3, Issue 2

Peter Sewell Peter.Sewell at cl.cam.ac.uk
Mon Feb 6 13:09:58 UTC 2017


On 6 February 2017 at 12:00,
<c-safe-secure-studygroup-request at lists.trustable.io> wrote:
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sun, 05 Feb 2017 21:55:35 +0000
> From: Paul Sherwood <paul.sherwood at codethink.co.uk>
> To: trustable-software at lists.trustable.io,
>         c-safe-secure-studygroup at lists.trustable.io
> Subject: [C-safe-secure-studygroup] The DeepSpec project...
> Message-ID: <70f9c1b2809a7c31e17495ffe40deb9c at codethink.com>
> Content-Type: text/plain; charset=US-ASCII; format=flowed
>
> Hi all,
> Edmund brought the DeepSpec project to my attention a couple of days
> ago, and I think it may be of interest both to the trustable community
> and Safe-Secure-C wizards.
>
> I find it particularly interesting to see research on bringing formal
> mathematical rigour to C language, tooling and interfaces.
>
> My own limited exposure to formal methods over the years has led to a
> couple of observations:

It's worth noting that there have been big changes in this area in the
last ten years or so, both in what's possible and in the kinds of
problems that people work on.  It's now feasible, in the context of a
substantial research project, to do full machine-checked correctness
proofs of nontrivial software - eg the CompCert verified compiler, the
seL4 kernel, the Vellvm LLVM verified optimisation passes, and many
other examples.  These are typically clean-slate implementations.
It's also feasible to do rigorous specification and testing against
such specifications for existing real-world abstractions - this can be
at a larger scale, but with less proof.  As some of you will know,
many of my colleagues have been doing this, in several domains:

- the C/C++11 concurrency model (working with the WG21 concurrency group)
- current work on sequential aspects of C (with WG14)
- the concurrency architectures of x86, ARM, and IBM Power processors
(with IBM and ARM)
- ELF linking
- JavaScript
- the TCP and TLS protocols
- POSIX filesystems

In particular, Kayvan Memarian and myself are on this list to see if
his Cerberus work on C semantics
(http://www.cl.cam.ac.uk/~pes20/cerberus/) can usefully be applied
here in future.

Much of this is currently funded by the REMS project, described at
http://rems.io
The communication gap you mention is certainly something that needs
care, but it's not a fundamental difficulty.

Peter


> - I've found it hard to have productive communication with advocates of
> formal methods: they probably conclude I'm too dumb for their concepts,
> while I conclude their concepts are likely to be too difficult for
> normal engineers
>
> - the communication gap makes me worried that formal methods folk may
> create solutions which are theoretically fantastic, but don't address
> practical realities
>
> However, as Niall said in the early discussions here [2] maybe the best
> we can do is to aim for trustability only for minority of core software,
> as a safe sandpit for the majority.
>
> In which case, maybe that core can (must?) be kept pure and isolated
> from typical real-world developers.
>
> br
> Paul
>
> [1] http://deepspec.org
> [2]
> https://lists.trustable.io/pipermail/trustable-software/2016-July/000005.html
>
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> C-safe-secure-studygroup mailing list
> C-safe-secure-studygroup at lists.trustable.io
> https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup
>
>
> ------------------------------
>
> End of C-safe-secure-studygroup Digest, Vol 3, Issue 2
> ******************************************************



More information about the C-safe-secure-studygroup mailing list