BIGV file format

[Alexander Senier]

Hi Doug,

sure, I'm happy to do that. We develop a toolset to partition security
protocol implementations into interacting components. Based on the
security guarantees (confidentiality, integrity) required by the
elements of the protocol we divide it into partitions. The idea is that
some partitions are untrusted and require no guarantees (e.g.
networking) while others do (encryption). If components are isolated and
interact over well-defined  interfaces only, errors in untrusted
partitions don't affect security critical ones. If we could do this for
large software automatically, this would greatly decrease the trusted
code size.

This is where Graal comes into play. So far, our models are derived
manually from a specification, which is tedious, error-prone and doesn't
scale. The idea is that we use an existing implementation of a security
protocol and build a sample app around it. For this application we
perform a data flow analysis between subprograms. We may, however, need
to analyze the control flow to identify security-critical branches  in
some cases  (e.g. when checking whether a signature was correct).

As for the our needs wrt. to the output format, the information I see in
IGV right now looks sufficient. I don't think we require any graph from
the compile steps after parsing for our purpose, so a dump level 0 with
only one graph per method would be nice. From the output, we need be
able  to unambiguously identify the methods invoked so that we can
annotate them (e.g. to mark the bounds of our model or map library
functions to known primitives). In the future, we may also want to map
back the log output to the source code to be able to create source code
for the components we  have identified.

A standard binary format for which libraries exist would be great. I
have no strong opinion on that - there are plenty of potential options
(CBOR, BSON, XDR...). What is slightly annoying for integration into an
automatic toolchain is the non-deterministic names of the log files. One
single   file with a fixed name would be nice here. But I guess that's a
multithreading issue and it's not super critical.

Hopefully I could make our intention clear. Thanks for asking! I'm
interested in feedback if you see a better way to obtain the information
we need.

Cheers,
Alex

On 06/12/2017 02:50 PM, Doug Simon wrote:
> Hi Alex,
> 
> Are you able to provide more information about the tool you are developing/using that reads the BIGV format? This may help guide us in terms of what's important.
> 
> -Doug
> 

-- 
Dipl.-Inf. Alexander Senier
Scientific Assistant

TU Dresden
Faculty of Computer Science
Institute of System Architecture
Chair of Privacy and Data Security
01062 Dresden

Tel.: +49 351 463-38719
Fax : +49 351 463-38255