wiki:WikiStart

CheckAPI



Write-Once, Run Anywhere?

Many APIs purport to support “write-once, run anywhere” (WORA) behavior, allowing application developers to write one implementation that will run on a wide variety of platforms. Unfortunately, subtle differences between the behavior of underlying platforms makes true WORA behavior difficult to achieve, so applications using these APIs can be plagued by bugs. This has led application developers to re-coin the phrase as “write once, debug everywhere.” These portability bugs can be particularly difficult to diagnose, because they arise from the API implementation, rather than from application code.


CheckAPI

CheckAPI, transparently monitors an application’s interactions with an API and compares the return value of methods to the expected WORA behavior. To do this, CheckAPI simulates execution of the API on a systems-style implementation model (SIM). A SIM can be created by modifying the API’s source code or written from scratch and is much simpler than the API implementation. CheckAPI uses several optimizations including revertible data structures and systolic trace disambiguation, to automatically and efficiently validate the WORA property on APIs used by complex, multi-threaded applications. We validated CheckAPI on applications using POSIX, JavaScript, and Repy, and detected dozens of WORA violations that are verified bugs in widely used software.

Access CheckAPI Source

You can get the CheckAPI through this link.
http://checkapi.poly.edu/projects/project/wiki/AccessCheckAPISource


Using POSIX CheckAPI

In order to use the CheckAPI implementation for POSIX, three steps have to be followed. First the user gathers traces. These traces are then parsed and the initial file state of the POSIX model is generated. The last step is the actual verification of traces with the CheckAPI system.

Gathering Traces

The first step in using the POSIX implementation of CheckAPI is to gather a trace from a machine, which will be later used as input for the verification step.

Gathering Traces in Linux

Traces in Linux can be gathered using the strace utility. The expected way of using strace to gather traces that can be parsed by our parser is:

$ strace -v -f -s1024 -o output_filename command

More information about gathering traces on Linux can be found here: https://checkapi.poly.edu/projects/project/browser/posix_checkapi/TRACES/Linux/README.

Gathering Traces in Solaris

Traces in Solaris can be gathered using truss. The expected way of using truss to gather traces that can be parsed by our parser is:

$ truss -f -rall -wall -vall -o output_filename command

More information about gathering traces on Solaris can be found here: https://checkapi.poly.edu/projects/project/browser/posix_checkapi/TRACES/Solaris/README.

Gathering Traces in BSD

A D script is provided, which can be used to gather traces on BSD systems. Usage:

$ dtrace_bsd.d -o <output_name.dtrace> -c "<command with arguments>"

Please note the quotes around the command and arguments. Also note that dtrace can only run with ROOT priviledges under BSD.

The D script (dtrace_bsd.d) and more information about how you set up DTrace on BSD (README) can be found here: https://checkapi.poly.edu/projects/project/browser/posix_checkapi/TRACES/BSD.

Gathering Traces in Mac OS X

Similarly to BSD Operating Systems, the Max OS X also provides the DTrace utility. A OSX version of the tracing D script along with a readme file are provided here: https://checkapi.poly.edu/projects/project/browser/posix_checkapi/TRACES/MAC_OSX/.

$ dtrace_osx.d -o <output_name.dtrace> -c "<command with arguments>"

Parse traces and generate initial FS

The parser should be executed from the same machine and directory where the traces are gathered. The parser can be found here: https://checkapi.poly.edu/projects/project/browser/posix_checkapi/TRACES/POT.

$ python parser.py trace_file (strace/truss/dtrace)

The last argument is optional and reveals the type of the trace.

The initial file system state is represented as a Lind FS. The latter is made up of a lind.metadata file and a set of linddata.# files. Once these files are genereated, a trace bundle is constructed which consists of:

  • the original trace file (strace or truss output file)
  • a file containing the parsed trace (a list of all parsed actions pickled)
  • the Lind FS files.

Run POSIX CheckAPI

Using the bundle created in the previous step, the verification part of the CheckAPI can be executed:

$ python verify-posix.repy <trace bundle> <error file>

Using Repy CheckAPI

CheckAPI's primary version uses security layers to interpose on API calls, log them and then verify them against a model of the API. The first step in using CheckAPI is to copy all of the required files from http://checkapi.poly.edu/projects/project/browser

If the application you are running with CheckAPI will try and open any existing files in the filesystem they must be added to the check_api_initial_filestate.input file that is used at initialization time of CheckAPI. If this is not done the model will not know that a given file exists but the implementation will, which will result in a conformance failure. It should be noted that any new files added to this file must be separated by a new line.

After this you checkout the CheckAPI Source, then you can run any application that supports Repy V2 with CheckAPI.

The current version CheckAPI using Socket as IPC in two processes. Therefore, you need to start two commands to running CheckAPI.

  1. Start the verification process as follow command.
    $ python repy.py restrictions.full dylink.repy check_api_verify.repy
    
  1. Start the interposition process as follow command:
    $ python repy.py <restrictions file> encasementlib.repy dylink.repy check_api.repy <program under test>
    

Running CheckAPI with Benchmark

When you Checkout all the source of CheckAPI, you can runing CheckAPI with Benchmark through this link:
http://checkapi.poly.edu/projects/project/wiki/RunningCheckAPIBenchmarks

Current Limitations

  • Currently looking into a method to reduce some false-positives for pending API calls.

Future Work

Core Model File System State:

  • Currently the user of CheckAPI must list in the check_api_initial_filestate.input file all of the possible files that an application may want to access on the filesystem. This can sometimes be difficult to tell if the applications you are using are ones that you did not make yourself. It may be nice for the CheckAPI core model to attempt to import a file into its model state if and only if it exists in the file system. For example:
    • If while in the middle of executing an application it calls openfile("repy.py", create=False) where repy.py was not listed in the check_api_initial_filestate.input file before execution this would normally cause an model conformance failure. This is because the model has no idea that this file exists in its file system where as the implementation checks the file system and opens it without any problem.
  • Where as an updated version of the core model, specifically the openfile() API call, would check the the filesystem (via the implementation openfile() call) to see if the file in question existed, if it does then it would import the file and its contents into the core model's in memory state.
  • It should be noted, however, that this could mask some bugs related to openfile reporting that a file exists when it shouldn't, or errors like this. I imagine these would be rare though.

API Calls Currently Not Verified by CheckAPI

Some API calls are not currently being verified by CheckAPI. Below is a list of the calls that are currently not supported with a brief explanation as to why they are not included. If an API call from FutureRepyAPI is not included in this list it means it is supported by CheckAPI.

  • sleep(), getruntime()
    • Not modeling time.
  • getthreadname()
    • Assumed correct for CheckAPI to work.
  • exitall()
    • Nothing to verify. However, this currently forces a final verification of other calls when executed.
  • createvirtualnamespace(code, name), virtualnamespace.evaluate(context)
    • Not modeling namespace calls.
  • getresources()
    • Some aspects of resources are being verified but not the getresources call itself.
  • getlasterror()
    • Not supported.
  • safelyexecutenativecode(binary, arglist)
    • Not modeling Lind related calls.

Unit Tests that are not supported with CheckAPI

A handful of repyv2 unit tests are not supported with CheckAPI. This is mostly because of resource usage assumptions that the unit tests have.

  • ut_repyv2api_fileclosereleasesresource.py
  • ut_repyv2api_filereadatperformsresourceaccounting.py
  • ut_repyv2api_filewriteatperformsresourceaccounting.py
  • ut_repyv2api_openfileconsumesfilehandles.py -> resources & listfiles issue.
  • ut_repyv2api_initialusevaluesaresane.py
  • ut_repyv2api_openfileperformsresourceaccounting.py
  • ut_repyv2api_listfilesperformsresourceaccounting.py
  • ut_repyv2api_removefileperformsresourceaccounting.py
  • ut_repyv2api_stoptimesaresane.py

Creating a SIM (model)

It is often easiest to construct a SIM by modifying a copy of the API's source code. This section will show you how this could be done for a tiny API called simplecrypto, which generates random ints that can be retrieved later.

simplecrypto.py

import os

# Previously retrieved random ints
previous = []

"""
Returns a random int between 0-255
"""
def getnewrandom():
  # Get random int
  num = int(os.urandom(1).encode('hex'),16)
  
  # Store random int for later calls to getpriorrandom(), and return
  previous.append(num)
  return num

"""
Returns a previously retrieved random int. If index is negative, raises
ValueError. If index is >= the number of random ints previously retrieved,
raises IndexError.
"""
def getpriorrandom(index):
  # Check for negative index
  if index < 0:
    raise ValueError
    
  # Check for index out of bounds
  elif index >= len(previous):
    raise IndexError
  
  return previous[index]

Let's look at the two functions separately. To model getnewrandom(), we first execute the implemented version above and store its result. Next, we use an oracle to verify that the result conforms to the specification: the return value should be between 0-255, and no Exceptions should be raised. You can see the oracle setter/getter code here: https://checkapi.poly.edu/projects/project/browser/repy_checkapi/CheckAPI/check_api_oracle_setter_getter.repy

simplecrypto_model.py (1 of 2)

# Previously retrieved random ints
previous = []

"""
Returns a random int between 0-255
"""
def getnewrandom():
  num = error = None
  
  # Get random int with the implementation
  try:
    num = simplecrypto.getnewrandom()
  except Exception as error:
    pass
    
  # Store result in the oracle
  oracle_setter(num, error)
  
  # Verify that the implementation's result is in [0,255] with no Exceptions
  try:
    oracle_getter(regex_cond_range(0, 255), None)
    
  # Display any detected model conformance failures
  except Exception as e:
    print type(e).__name__ + ': ' + str(e)
    exit()
  
  # Store random int for later calls to getpriorrandom(), and return
  previous.append(num)
  return num

The process to model getpriorrandom() is nearly identical, except now we verify that Exceptions are raised in the appropriate circumstances.

simplecrypto_model.py (2 of 2)

"""
Returns a previously retrieved random int. If index is negative, raises
ValueError. If index is >= the number of random ints previously retrieved,
raises IndexError.
"""
def getpriorrandom(index):
  impl_num = impl_error = None
  
  # Retrieve previous random int with the implementation
  try:
    impl_num = simplecrypto.getpriorrandom(index)
  except Exception as impl_error:
    pass
    
  # Store result in the oracle
  oracle_setter(impl_num, impl_error)
  
  # Verify that the implementation's return value and/or Exceptions are correct
  try:
    # Check for negative index
    if index < 0:
      oracle_getter('None', [ValueError])
      
    # Check for index out of bounds
    elif index >= len(previous):
      oracle_getter('None', [IndexError])
    
    # Retrieve the prior random number, verify the implementation's value
    else:
      prev = previous[index]
      oracle_getter(regex_cond_range(prev, prev), None)
    
  # Display any detected model conformance failures
  except Exception as e:
    print type(e).__name__ + ': ' + str(e)
    exit()
  
  return impl_num
Last modified 20 months ago Last modified on Jan 7, 2016 10:28:00 AM