$blog→errstr

do not commit

On Static Program Analysis

| Comments

Introduction

As I stated in my previous post, my undergraduate thesis is on static program analysis of Android applications to prove malicious behavior. In this article, I try to explain what static program analysis is and isn’t and the rational behind using using it for this research. Oh, and there is code to look at, too!

Static Analysis of Android: Introduction

| Comments

Introduction

Malware on Android is a problem. With over 500 million activated devices, it is a large user base to attack and the Android Market is a great delivery mechanism. Even though Google has started to scan applications uploaded to the marketplace, there still has been an up-tick in malware. This raises the central question I am addressing in my Undergraduate Thesis: Can an Android application be proven to be non-malicious by small step analysis?

This article starts off a series of articles that I will be writing over the course of the next few months investigating this question through my research with the U-Combinator group at the University of Utah. The group is determining, through static analysis, how much can be proven about the nature of any Android application in an effort to provide a relatively-provable secure Android environment. To get started, this article gives an overview of what makes up an Android application.

Reduction

| Comments

Introduction

Two of the most common forms of reduction are Call-By-Name (CBN) and Call-By-Value (CBV), with the latter being the most ubiquitous. In this post, I give implement both in Racket.

Mathematical Definitions

### Non Deterministic Full ß-reduction This is a non-deterministic, full ß-reduction definition. Notice that there is no value term definition, that is because a value cannot be a ß-redex. The way to read the following rules are, the definition on top of the line is the conditional, on the bottom is what happens if that is true.