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.
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
Choose the target
Build LogicDroid.
1. Set up environment
2. Update API
2. Build the code
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
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
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.
Set up Environment
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
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.
VIDEO
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
VIDEO
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.
LogicDroid from Android Security Project: Data-dependent security polices
1. Demo video
VIDEO
LogicDroid from Android Security Project: On-the-fly policies update
Original LogicDroid Project
1. Demo Video
VIDEO
Source: Hendra Gunadi Home Page