Analyzing DLLs using Seal

Seal takes as input DLL(s) obtained by compiling C# code bases. The main executable that starts the analysis is called "Checker.exe" and can be found in the "$SEALHOME\Bin" directory. To analyze a dll named input.dll stored in the directory "C:\" use the following command:

$SEALHOME\Bin\Checker.exe /in C:\input.dll

To analyze multiple DLLs that are inter-dependent follow the steps detailed below:
  • Sort the DLLs in the order of their compile time dependencies. Note that the compile time dependencies are always acyclic. Given n DLLs it is always possible to number them as d1 to dn such that each di depends (compile time dependence) only on d1, d2 ... to di
  • Provide all the inputs simultaneously to Seal, in the order of their dependencies, as illustrated below: $SEALHOME\Bin\Checker.exe /in d1 /in d2 ... /in dn

Configuring Seal

Seal allows the users to configure the analysis by exposing some parameters to the users.
Seal can be provided an optional Config file containing values for the parameters.
For example, see the config files stored in the directory "$SEALHOME\Configs".

To provide a config file to seal use the following command:

Checker.exe /in "input-dlls" /config-file "path-to-config-file"

If no config file is provided Seal uses the default configuration specified in $SEALHOME\Configs\default.config file


Here, we discuss the parameters that can be specified in the config file. (There are some additional parameters not explained here . Users can ignore them. They are mainly used for development/debugging purposes).

Parameters that control the outputs of the analysis

  • DumpProgressToConsole (Boolean) := When set to true dumps the analysis progress which is the percentage fraction of the procedures that have been analysed out of the total number of procedures in the input DLL.
  • DumpAsVSErrorMsg (Boolean) := When set to true dumps the results of the analysis to the console in VS error message format: (line-number, column-number) error-message. The line and column numbers will be displayed correctly only when the PDB files for the DLL are also provided to the analysis. The PDB files should be present in the same directory as the DLL.
  • DumpSummariesAsGraphs (Boolean) := When set to true outputs the summary graphs computed during the bottom-up phase of the analysis as DGML files. The DGML files can be browsed using visual studio.
  • DumpWholeProgramCallGraph (Boolean) := When set to true dumps the call-graph of the analysed DLL on completion. The call-graph is dumped in a custom textual format. As of now we do not support any standard graph formats. The call-graph does resolve delegate calls, virtual calls etc. using the summaries computed by the analysis.
  • UnaCallsFilenameSuffix (a suffix of a filename like "-una-calls.txt") := The list of unanalyzable calls that are encountered during the analyses are written to a file. These are calls whose targets are not analyzable e.g. because they are defined in a different DLL not provided to the analysis or because they are calls to native methods. This parameter specifies the suffix that needs to be appended to the output file. The first part of the filename is the name of the analyzed DLL.

Serialization Parameters

  • SummarySerialization (Boolean) := When set to true, the analysis serializes the types and procedure summaries to the database. This allows the subsequent analyses to use the summaries.
Note: the summaries once searialized remain persistent unless they are explicitly deleted from the database.
We use MS SQL compact 3.5 database to store the summaries. The database can be found in the DBs directory inside the $SEALHOME. The database uses four tables (relations). Every entry in the tables stores the name of the dll, that created the entry, in the field 'dllname'. One can use this field to (manually) clear the information corresponding to a dll, if necessary.
An alternative is to re-analyze the DLL by setting the "ClearDBContents" flag (explained below) to true.
  • WitnessSerialization (Boolean) : When set to true, serializes the side-effects computed by the analysis to a file using the BinarySerializer. This is mainly used in testing for comparing the outputs of the tool with the expected outputs.

Parameters that control the precision/scalability of the analysis

  • FlowSensitivity (Boolean) := When set to true runs the analysis in the flow-sensitive mode. We recommend to have this flag set to true. However, if the analysis does not scale within the available time/resources, try setting the flag to false.
  • BoundContextString (Boolean) = The analysis associates a context string with the names of the abstract heap objects for capturing the context under which the objects are created. This improves the context-sensitivity of the analysis.
The calling context is a set of call-strings in our analysis. Setting the flag to false indicates that the size of the set is unbounded and so the analysis tracks the full (acyclic) context under which an abstract object is created. However, this may (severely) slow down the analysis on large programs.
This flag when set to true informs the analysis that the context-string has to be bound. The actual bound can be set using the following parameter.
  • ContextBound (a non-negative integer) := This flag has a meaning only when BoundContextString is set to true, it is ignored by the analysis otherwise. By default, this is set to 1. However, it can be increased further to improve precision at the expense of scalability or can be set to zero to improve scalability at the expense of precision.

Input file paths

The following are additional parameters to the analysis. We recommend not to change the values of these parameters.
  • BenignSideEffectsFilename := Specifies the path (relative to $SEALHOME) to the file containing a set of side-effects that are benign and can be ignored.
  • StubMappingFilename := Specifies the path (relative to $SEALHOME) to the file that provides the mapping from the classes and methods to their corresponding stubs (if any). The file has a fairly sophisticated format. Do not tamper with this file.
  • DB := Meant to be a constant "FILE"
  • ClearDBContents := When set to true clears any information stored in the database for the input DLL on completion of the analysis
  • DBFilename := Specifies the path (relative to $SEALHOME) to the database file

Last edited May 24, 2014 at 7:56 PM by Ravi87, version 22


No comments yet.