bluespec.com Forum Index bluespec.com
Bluespec Forums
 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister 
 ProfileProfile   Log in to check your private messagesLog in to check your private messages   Log inLog in 

compiler certification?

 
Post new topic   Reply to topic    bluespec.com Forum Index -> Tools: BSC (Bluespec Compiler)
View previous topic :: View next topic  
Author Message
NCCMoore



Joined: 10 Jul 2012
Posts: 6

PostPosted: Mon Apr 22, 2013 11:58 am    Post subject: compiler certification? Reply with quote

Hello everyone,

My research group and I are currently investigating BSV for use in some safety critical applications. I was wondering if the Bluespec Compiler has any verification and validation qualifications, or has been certified in any way, or if there is a correctness proof floating around somewhere.

My search has so far been fruitless, and I was wondering if anybody here might be able to point me in the right direction.

Additionally, if anyone has any examples of BSV being used in existing safety critical applications that would interest me enormously.

Thank you for your time,

--Nick
Back to top
View user's profile Send private message
nikhil
Site Admin


Joined: 23 Jul 2007
Posts: 14
Location: Waltham, MA

PostPosted: Mon Apr 22, 2013 5:32 pm    Post subject: Reply with quote

Hello, Nick:

No, we do not have any certification of our tools for safety-critical systems.

That said, we have a strong heritage in formal verification, and there
are a number of ongoing activities. Here is a chronological listing
that I am aware of:

- BSV's roots are in formal verification (even before synthesis!).
Our behavioral model (atomic transactional rewrite rules) was
originally chosen by Xiaowei Shen, Arvind, Stoy et. al. at MIT
in the late 1990s for formal specification of correctness of
deeply pipelined processors, and of distributed cache coherence
protocols (I can provide refs on request). The technology to
synthesize these directly came later (the original core of BSV
technology).

- Dom Richards at U.Manchester did a Ph.D. thesis in which translated
BSV into PSV and SAL and conducted proofs of some small examples.

- SRI and U.Cambridge (UK) are currently doing a DARPA-funded project
for a processor architecture with formal proofs of correctness
of security policies. Their architecture extends the MIPS ISA
with capabilities for security checking. The architecture has
been implemented, and runs of FPGAs with NetBSD as an OS. The
processor is implemented in completely in BSV. The formal
verification part has so far been focused on
tool-building. Specifically, they take a lambda-calculus-like
intermediate form of the BSV description of their processor
(this IF is an output from our compiler), and automatically
create an abstraction that only involves architectural state
(i.e., hides all other microarchitectural state). This
abstraction is then used to conduct proofs. They have not
published much on this to date (since they've had a long ramp-up
on tool building), but some information is in their poster at a
recent DARPA meeting:

http://www.csl.sri.com/users/neumann/20121113-ctsrd-sandiego-poster.pdf

Nirav Dave at SRI is the principal researcher driving the formal part.

We (Bluespec) expect that the infrastructure developed in this
project, which link our tool to SRI's formal tools, will become
a standard part of our tools.

- UPenn is also working on a DARPA-funded project to develop a
processor architecture with formal proofs of security and
information-flow properties. Like SRI/U.Cambridge, they have
also chosen to implement in BSV. Unlike SRI/U.Cambridge, who
started with the MIPS ISA, they have chosen to go with a
clean-slate design. Andre Dehon and Benjamin Pierce are the
principals in this project, AFAIK. This is a younger project
than the SRI/U.Cambridge one, and so they have not made as much
progress yet. Their web site is:

http://www.crash-safe.org/

Best regards,

Nikhil
(CTO Bluespec)
Back to top
View user's profile Send private message AIM Address
NCCMoore



Joined: 10 Jul 2012
Posts: 6

PostPosted: Tue Apr 23, 2013 11:28 am    Post subject: Reply with quote

Dear Dr. Nikhil,

Thank you for your swift and thorough reply. To be honest it was the paper by Richards and Lester that initially grabbed our attention.

We're currently working with the nuclear industry to develop safety critical FPGA systems, and BSV seems like it could save us a lot of hassle, we're just trying to sort out the toolchain (which ideally would include BSC as a trusted component).

Thanks again for your time and all the valuable information,


--Nick
Back to top
View user's profile Send private message
Display posts from previous:   
Post new topic   Reply to topic    bluespec.com Forum Index -> Tools: BSC (Bluespec Compiler) All times are GMT - 4 Hours
Page 1 of 1

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You can attach files in this forum
You can download files in this forum
bluespec.com topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group
Protected by Anti-Spam ACP