EviCheck: Digital Evidence for Android

EviCheck is a tool for the verification, certification and generation of lightweight fine-grained policies for Android. It uses a lightweight static analysis to show the conformance between policies and application behaviour.

A distinguishing feature of EviCheck is its ability to generate digital evidence: a certificate for the analysis algorithm asserting the conformance between the application and the policy. This certificate can be independently checked by another component (tool) to validate or refute the result of the analysis. The checking process is generally very efficient compared to the certificate generation.

Policy Language

A policy in Evicheck consists of a set of rules of the form ([] means optional)

[∼]CONTEXT_1,..,[∼]CONTEXT_m  : [∼]PERM_1,..,[∼]PERM_n, [∼]API_1,..,[∼]API_k

CONTEXT_i ∈ { EVICHECK_ENTRY_POINT, EVICHECK_ACTIVITY_METHOD, EVICHECK_SERVICE_METHOD, 
	  EVICHECK_RECEIVER_METHOD, EVICHECK_ONCLICK_HANDLER, EVICHECK_ONTOUCH_HANDLER, 
	  EVICHECK_DO_INBACKGROUND, EVICHECK_ONCREATE_METHOD, EVICHECK_START_METHOD, EVICHECK_RESTART_METHOD
	  EVICHECK_PAUSE_METHOD, EVICHECK_RESUME_METHOD, EVICHECK_DESTROY_METHOD, EVICHECK_STOP_METHOD }

PERM_i's are Android permissions

Verifying Apps

EviCheck operates in different modes. In the verification mode mode, it takes an app together with a policy as input, and answers whether the policy is satisfied by the app and eventually outputs a certificate (digital evidence). EviCheck also returns diagnosis pointing to the first violated rule of policy. For example given the app Recorder.apk, we call EviCheck as follows:

python2.7  EviCheck.py -f Recorder.apk -g -p recorder.pol -m -t recorder.cert

We are asking EviCheck to check if the app Recorder.apk obeys the policy recorder.pol and it should generate a certificate in the file recorder.cert. The file recorder.pol contains only one rule

EVICHECK_ENTRY_POINT ~EVICHECK_ONCLICK_HANDLER : ~RECORD_AUDIO

It says that permission RECORD_AUDIO should not (~ for negation) be used in any entry point except click handlers. As a result we obtain

	Policy valid!
	============================
	APK file:  Recorder.apk
	Analysis time:  0.000204086303711
	Policy checking time:  0.000418901443481
	Number of rules:  1
	Number of valid rules:  1
	Number of violated rules:  0
	Number of methods:  73
	============================

meaning that the policy is respected by the app. Let us now try to verify another Recorder_bad.apk, we call EviCheck as follows:

python2.7  EviCheck.py -f Recorder.apk -g -p recorder_bad.pol -m -t recorder.cert

and we obtain

     Rule 1  ==>  set(['~EVICHECK_ONCLICK_HANDLER', 'EVICHECK_ENTRY_POINT']) : set(['~RECORD_AUDIO'])
     Policy violated! Tag RECORD_AUDIO is in .../AudioRecordingActivity->onCreate(Landroid/os/Bundle;)V

Which means that the policy is violated, in addition to that we get the location where the rule is violated, namely the method .../AudioRecordingActivity->onCreate(Landroid/os/Bundle;)V

Certificate Checking

In the certificate checking mode, EviCheck takes as input an app, a certificate and a policy, and returns a message indicating whether the certificate is valid. It also returns diagnosis pointing to the first inconsistent entry in the certificate. Let us check if the previously generated certificate recorder.cert is valid. We write

python2.7  EviCheck.py -f Recorder.apk -c -p recorder.pol -m -t recorder.cert

We are using the option -c (checking) instead of -g (generation), as this tells EviCheck to check the certificate recorder.cert. We obtain the answer

    Certificate valid!
    Policy valid!
    ============================
    APK file:  Recorder.apk
    Analysis time:  0.000132083892822
    Policy checking time:  0.000275135040283
    Number of rules:  1
    Number of valid rules:  1
    Number of violated rules:  0
    Number of methods:  73
    ============================

Meaning that the certificate is valid as well as the policy.

Policy Generation

To release the user from the burden of writing anti-malware policies, EviCheck offers the option of generating them automatically. This requires a training set of malware and benign applications whose specifications will be extracted. A specification is a summary of the usage of different permissions in various contexts within an app. They somehow represent a condensed (compressed) form of the generated certificate. For illustration, we consider again the app Recorder and we call EviCheck as follows:

python2.7  EviCheck.py -f Recorder.apk -g  -m  -r recorder.spec

The option -r indicates that the specification of the app must be generated and stored in the file recorder.spec which looks like:

    //----------------------------------------------------------
    //----------------------- Recorder.apk
    //----------------------------------------------------------
    EVICHECK ACTIVITY METHOD : RECORD AUDIO
    EVICHECK ONCREATE METHOD :
    EVICHECK ONCLICK HANDLER : RECORD AUDIO

The specification simply says that the permission RECORD AUDIO is used in a click handler and in an activity. As mentioned previously, to infer the policy we require a training set of benign and malware applications. The goal is to find a policy under which a maximum of malware is excluded and a maximum of benign applications is allowed. We formulate this as an optimisation problem and the pseudo Boolean solver Sat4j is used as backend to solve it. For this EviCheck takes as input two files containing a batch of specifications, one for benign apps spec.ben and the other one for malware spec.mal. We then call EviCheck as follows:

python2.7 EviCheck.py -s spec -p my_policy.pol

The generated policy is stored in the file my_policy.pol.

Table Of Contents

EviCheck: Digital Evidence for Android

Policy Language

Verifying Apps

Certificate Checking

Policy Generation