Publications

Xiaoning Du, Yang Liu and Alwen Tiu. Trace-Length Independent Runtime Monitoring of Quantitative Polices in LTL. In FM 2015, LNCS Vol. 9109, pp. 231 - 247, Springer, 2015.

Hendra Gunadi and Alwen Tiu. Android Security: A Case for Runtime Verification.Unpublished notes, 2015.

Hendra Gunadi and Alwen Tiu. Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system. in FM 2014, LNCS vol. 8442, pp. 296-311, Springer, 2014.

LogicDroid Source Code

This section describes how to set up your local work environment to build the LogicDroid source files. You will need to use Linux.

Follow these instructions to establish build environment for Android: Source

On Ubuntu, Java SE 1.6 is required to compile the source code.

Set up Environment


$ . build/envsetup.sh

Choose the target

lunch 1

Build LogicDroid.


1. Set up environment

2. Update API

$ make update-api

2. Build the code

$ make -j4

LogicDroid system image directory after compilation:

<LogicDroid_directory>/out/target/product/generic/system.img

More about building Android Source Code: https://source.android.com/source/building.html

Build LogicDroid Kernel.


Require Prebuilt gcc from Android Source

$ CROSS_COMPILE=<LogicDroid_directory>/prebuilt/linux-x86/toolchain/arm-eabi-4.4.3/bin/arm-eabi- ARCH=arm make -j4

LogicDroid kernel image directory after compilation:

<kernel_directory>/arch/arm/boot/zImage

Build the SDK.


1. Set up environment

$ . build/envsetup.sh
$ lunch sdk-eng

2. Build the SDK

$ make sdk –j8

The location of SDK:

<LogicDroid_directory>/out/host/linux-x86/sdk

Run LogicDroid Emulator.


1. Set up environment

2. Run the emulator

$ emulator -system <system_image_directory> -kernel <kernel_image_directory> -show-kernel

More about Android Emulator: http://developer.android.com/tools/help/emulator.html

LogicDroid Components

Policy Monitoring


Policy Monitoring is a Java software which is used to generate the policy input string for LogicDroid.

Arguments

$ java GenerateMonitor <policy_xml_file> <debugMode>

Debug Mode:

Default (0) : Print breakdown input string and hard source code in the old kernel (Original Version)

1 : Print only breakdown input string

2 : Print input string

When running, Policy Monitoring will automatically generate Monitor.c. This file is used to simulate logic of the Monitor inside the kernel.

LogicDroid on Galaxy Nexus

Set up Environment


$ . build/envsetup.sh

Choose the target

$ lunch full_maguro-userdebug

Build LogicDroid for Galaxy Nexus


1. Download the Galaxy Nexus drivers: Download

2. Extract and Install the Galaxy Nexus drivers

3. Setup the environment and build normally

Note: The system calls are different for the Maguro kernel.

Build Galaxy Nexus kernel (Maguro)


1. Download the Galaxy Nexus kernel (Maguro): Download

2. Follow the Goldfish kernel build steps.

Note: The system calls are different with the goldfish kernel.

Flash Galaxy Nexus Image


1. Enable USB debugging (Settings -> { } Developer options -> USB debugging)

2. Enter bootloader

$ ./adb reboot-bootloader

3. Unlock OEM

$ ./fastboot oem unlock

4. Flash kernel (boot image)

$ ./fastboot flash boot <boot.img_directory>

5. Flash kernel (zImage)

$ ./fastboot flash zimage <zImage_directory>

5. Flash system image

$ ./fastboot flash system <system.img_directory>

5. Flash user data image

$ ./fastboot flash userdata <userdata.img_directory>

Demo video


LogicDroid prevents CureSec bug.

LogicDroid Apps

The following applications are used in LogicDroid project.

Security Controller


A policy editor application called Security Controller was developed to simplify the process. By providing the graphic UI, the Security Controller is able to automatically generate the policy and set the related predicates for each application according to the setting make by Android end users. Instead of writing complex policies in XML notations, the users can gain ease control by manipulating several switch buttons and checkboxes.

1. Demo Video

Bugs & Known Issues

1. To make sure LogicDroid work properly, the process com.android.browser needs to be forced stop whenever calling the method renewMonitorVariable or chaging the policy (Important when testing with com.android.browser). This issues seems to happen with the emulator running on low-performance computer.

2. Exist and ForAll Operator need to optimized.

Older Versions

LogicDroid from Android Security Project: Data-dependent security polices


1. Demo video

LogicDroid from Android Security Project: On-the-fly policies update


Original LogicDroid Project


1. Demo Video

Source: Hendra Gunadi Home Page