Thursday, December 29, 2011

Dalvik Virtual Machine & DEX Bytecode

Are you interested in Dalvik virtual machine and/or DEX bytecode? As you may know, Android application is eventually compiled into DEX bytecodes running on Dalvik virtual machine. 

Here are several interesting starting points you must know particularly if you like to hack Android applications.

Sunday, December 04, 2011

Making Android NFC Demo work.

This is a short article on how to make NFC Demo work. The NFC Demo is one of Android samples available from either the Android developer site or your local folder after installing Android SDK 2.3.3 or higher.

  - http://developer.android.com/resources/samples/NFCDemo/index.html
  - C:\Program Files\Android\android-sdk\samples\android-10\NFCDemo (in Windows)

The NFC Demo uses some Google collection library, which is available in

  - http://code.google.com/p/guava-libraries/

First, download guava-10.0.1.jar, which is the version I see at the time of writing this article.

Second, you create a new Android project, say, named NFCDemo. You don't need to create an Activity, so you uncheck "Create Activity" during your set up.

Third, once you created an android project, you  copy all files under the src and res in the NFCDemo sample to your project. Don't forget to overwrite AndroidManifest.xml in your project with that in the sample.

Of course, you have to add the downloaded guava-10.0.1.jar to the external jar path of your project.

That's it! Now you are ready to run it on Android Emulator.

If you have any questions, please post them as a comment to this article.

Tuesday, September 13, 2011

Data Synchronization

Data synchronization is the process of establishing consistency among data from a source to a target data storage and vice versa and the continuous harmonization of the data over time. It is fundamental to a wide variety of applications, including file synchronization and mobile device synchronization e.g., for PDAs.

http://en.wikipedia.org/wiki/Data_synchronization

The problem of synchronizing data is known as set reconciliation problem in Information theory.

http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1226606

In computer programming, bidirectional transformations (bx) are programs whose code express a transformation both from input to output and back to the corresponding input (possibly with modifications) in a single piece of code. Bidirectional transformations can be used to maintain several sources of information consistent, and to provide an abstract view to easily manipulate data and write them back to their source.

http://www.cs.cornell.edu/~jnfoster/papers/grace-report.pdf
http://en.wikipedia.org/wiki/Bidirectional_transformation

Monday, August 22, 2011

A Special Issue on Formal Proof in Notices of the American Mathematical Society (December, 2008)

Using computers in proofs both extends mathematics with new results and creates new mathematical questions about the nature and technique of such proofs. The special issue of Notices of the American Mathematical Society features a collection of articles by practitioners and theories of such formal proofs which explore both aspects.


  • Formal Proof by Thomas Hales
  • Form Proof -- The Four-Color Theorem by Georges Gonthier
  • Formal Proof -- Theory and Practice by John Harrison
  • Fromal Proof -- Getting Started Freek Wiedijk




Sunday, July 31, 2011

Supplements

Supplements for Submission to ICCE 2012, "A Secure Application Invocation Mechanism in Mobile Phones for Near Field Communication" :

Tuesday, May 17, 2011

Scheme Implementations in Java

Scheme is a small but very powerful functional language. The small size makes it easy to be ported everywhere. It started running on Android now.

List of Scheme implementations in Java (initially excerpted from here)

Schemes on Android

Roughly speaking, there seem to be two approaches to make Scheme run on Android. The first approach is to use Scheme for building Android package (APK) file. The other approach is to have some wrapper Android program that invokes the "eval" function to run a given Scheme program.

One of differences between them is that the former requires the installation process before one runs Scheme programs while the latter does not. Which approach is good? It must depends on what you want. If you like to program Scheme but want to run it on Android, the first approach is yours. If you are thinking of something like agent systems where small pieces of codes (agents) are wandering around different devices such as PCs, mobiles, TVs, and so on, you may prefer the second approach.

Here are some examples for the approaches.
  • The Scheme-as-Apk approach
  • The Scheme-as-agents approach

Thursday, May 12, 2011

OpenStack

OpenStack is an open source software to build private and public clouds.

http://www.openstack.org

This is a collection of open source technologies delivering a massively scalabl cloud operating system. OpenStack is currently developing two interrelated projects: OpenStack Compute and OpenStack Object Storgage. The former is software to provision and manage large groups of virtual private servers, and the latter is software for creating redundant, scalable object storage using clusters of commodity servers to store terabytes of even petabytes of data.


Wednesday, May 04, 2011

Sunday, May 01, 2011

Prototype: an Object-Oriented JavaScript Framework

Prototype is a JavaScript framework that aims to ease development of dynamic web applications. It offers a familiar class-style object-oriented framework, extensive Ajax support, higher-order programming constructs, and easy DOM manipulation.

http://www.prototypejs.org/

Friday, April 22, 2011

OpenSMT


1. SMT

SMT is an abbreviation of Satisfiability Modulo Theories. The SMT problem is a decision problem for formulas with respect to theories expressed in classical first-order logic with equality.

For example, a > 10 is a formula. Is this True or False? Obviously, we cannot answer this because it is neither True or False. The truth of the formula depends on what a is. Therefore, a question better than the previous one here is whether or not the formula is satisfiable. If it is so, we may be curious about when it is satisfiable, in other words, what is a model for the formula. An answer is that the formula is satisfiable when a is 11. An SMT solver will produce this kind of answer automatically.

The SMT problem is a combination of the boolean satisfiability problem (SAT) with an arbitrary theory. In the above example, we had SAT with an integer arithmetic theory. To solve the above example, it is not difficult to imagine that we need to use both a SAT solver and a decision procedure in Linear algebra such as the simplex algorithm. Another example formula may be (a and ((x + y <= 0) or not a) and ((x = 1) or b), which may explain better the necessity of the two solvers.

2. OpenSMT

The OpenSMT is an effort to build an SMT solver under the open source policy. This contrasts to most of the other SMT solvers, which are proprietary, such as Z3.
The OpenSMT provides a SAT solver, which is based on another cool open source MiniSAT, and it supports several theories including QF_UF, QF_IDL, QF_RDL, QF_LRA, QF_BV, F_UFIDL, and QF_UFLRA. For example, QF_UFLRA is a theory combination of uninterpreted functions and linear arithmetic on the rationals.

The OpenSMT combines each pair of the SAT solver and a decision procedure on one of the theories using DPLL framework. The DPLL algorithm is a complete, backgracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e., for solving the CNF-SAT problem. (DPLL denotes the names of early scientists Martin Davis, Hilary Putnam, George Logemann and Donald W. Loveland.)

The OpenSMT offers a set of C++ APIs to extend itself with a decision procedure on a theory. The theories mentioned above are integrated using those APIs. This way the OpenSMT opens its architecture to everyone and every  theory. 

The OpenSMT is capable of computing models and proofs. In case of formulas in SAT, it computes assignments to satisfy them to be True. It prints models in SMT-LIB syntax such as (= x 1) and (not b). It also prints models in the resolution proof format, which can guide a proof to lead to True. Given an unsatisfiable conjunction, the OpenSMT is able to generate a sequence of inferences that lead to a contradiction. 

Thursday, April 21, 2011

Processing


Processing is an open source programming language and environment for people who want to create images, animations, and interactions. Initially developed to serve as a software sketchbook and to teach fundamentals of computer programming within a visual context. Processing also has evolved into a tool for generating finished professional work. Today, there are tens of thousands of students, artists, designers, researchers, and hobbyists who use Processing for learning, prototyping, and production.


http://processing.org/

Friday, January 28, 2011

Automatic Client-Server Partitioning


The automatic client-server partitioning is a technique to partition an application functionality across the client-server boundary automatically.

Some of systems supporting the automatic client-server partitioning include:

  • Hilda
  • Links
  • Swift

Thursday, January 27, 2011

OKL4 (or seL4) Released.


On January 21st, 2011, there was an announcement that Open Kernel Labs released OKL4 Verified for download and prototyping.

http://www.ok-labs.com/releases/release/open-kernel-labs-provides-okl4-verified-for-download-and-prototyping


1. What are released

The seL4 ARM binaries both on ARM and IA32 are released. For each architecture, two binaries are available: one for debug mode and the other for release mode.

It provides the source codes for user libraries to make use of the released binary kernels. One can build several examples to pack it with the seL4 kernel to run on a version of Qemu supporting ARM architecture. For this, it provides an Elf loader (ARM boot loader) and a binary file manipulator (Dite).

A para-virtualised Linux, Wombat, is also included as an example. But it can run either on a Qemu supporting IA32 or a real hardware.

Open Kernel Labs released the seL4 Reference manual for API version 1.1 together with an abstract formal specification for the APIs. The specification is written in Isabelle/HOL definitions.

1.1 What are not released

Note that the source code for the seL4 kernel is not opened. As a natural consequence, it provides no concrete formal specification and no proof things. It is unfortunate not to be able to see a high-level prototype, written in Haskell, of the seL4 kernel that matches with the released abstract specification.

2. Playing with the seL4 examples

It seems to be quite straightforward to run the released seL4 examples. I ran them on Ubuntu 10.04. You have only to follow the instructions guided by

Some of the released examples run on ARM while the others run on IA32. You had better download two set of Code Sourcery toolchains. (Can we build the IA32 examples with the gcc compiler on the Ubuntu?)

This is just for your reference, I downloaded two Sourcery G++ Lite 2010.09-50 for ARM GNU/Linux and 2010.09-44 for IA32 GNU/Linux to build the released examples.

My quick trials succeeded in building and running the examples in Section 1,2,3,4, but got stuck in Section 5 and 6. (I will continue to explore the reason of the build errors I met.)

3.

(Soon I will try to write a summary of the API reference and the abstract specification.)

Wednesday, January 26, 2011

Quantifier Elimination

Quantifier elimination is a method of transforming a formula into an equivalent quantifier-free formula. Since quantifier-free formulae are easy to reason, quantifier elimination is useful for deduction and many quantifier-elimination procedures have been developed. Above all, quantifier-eliminationprocedures called "quantifier elimination by virtual substitutions" are known to be suitable for practical implementation. The idea of the virtual substitution based methods is to use a finit set of test cases, called an elimination set.

Emscripten: an LLVM-to-JavaScript compiler

It is very stunning to find Emscripten, a compiler of LLVM bitcodes into JavaScript. The LLVM bitcodes can be generated from C/C++ using llvm-gcc or clang or any other languages that can be converted into LLVM. The generated JavaScript can run on the WEB!

http://code.google.com/p/emscripten/



Wednesday, January 05, 2011

Near Field Communication (NFC)

What is NFC


Simply speaking, it is a technology that combines the funtion as a RFID tag and the function as a RFID reader! NFC defines three communication modes: peer-to-peer mode, read/write mode, and NFC card emulation mode. 

Standards
  • ISO/IEC 14443 : Identification cards, Contactless integrated circuit cards, Proximity cards
  • ISO/IEC 18092 : NFCIP-1 (NFC Interface Protocols) http://www.nfc-world.com/en/about/ ì°¸ê³ 
  • JIS X 6319-4 : FeliCa
  • ISO/IEC 15693 : Vicinity cards


Research Institute

NFC Implementations


Android NFC API supports Read NDEF messages, and SUN JSR-257 supports read/write mode and NFC card emulation mode. NFCIP and Libnfc support peer-to-peer mode in Java and in C, respectively.

 Workshop



News on 2011's NFC

Products
NFC Applications