[racket] static analysis for finding vulnerabilities on non-executable and untyped language

From: J. Ian Johnson (ianj at ccs.neu.edu)
Date: Wed Jun 4 10:05:31 EDT 2014

If you can't execute programs in the language, there are no vulnerabilities. So your analysis is 

(define (vulnerable? program) #f)

It just isn't "available" in the A of security's CIA (confidentiality, integrity and availability).

In all seriousness, you'll want to learn about semantics. What does your AST /mean/? How does it behave? Only then can you make predictions about its behavior with a static analysis.
A good place to start is the PLT redex book
http://www.amazon.com/Semantics-Engineering-Redex-Matthias-Felleisen/dp/0262062755/ref=sr_1_1?ie=UTF8&qid=1401889682&sr=8-1&keywords=plt+redex

After that, take a look at the technique, "Abstracting Abstract Machines" (AAM) to turn your redex models into sound analyses:
http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=8669075

The AAM paper does not discuss implementation, so we wrote a follow-up:
http://www.ccs.neu.edu/home/ianj/johnson-labich-might-van-horn-2013.html

After that, you'll want to know how to make precise abstractions of base types like numbers and strings. This is a big area with many solutions. The bibliography of the Astrée static analyzer may help you trim down your search for effective abstractions:
http://www.astree.ens.fr/

The abstract domains in Astrée do not just represent the possible values of one variable, but instead improve precision by /relating/ them to one another (a so-called relational domain). Astrée is specialized to first-order programs without dynamic allocation. AAM allows both, so this has been written on relational domains in AAM:
http://matt.might.net/papers/liang2013entangled.pdf

After that, you may be concerned with how data is used. Are you respecting privacy policies? Is it possible to read a user's email and then send it to a private server without the user's consent? This is the topic of information flow security, which has both problems of specifying policies and enforcing them. Take a look and Shuying Liang's work on the subject:
http://www.cs.utah.edu/~liangsy/spsm53-liang.pdf

After that, if you are not satisfied, it's time to get a PhD further extending the field.

-Ian
----- Original Message -----
From: "Mansour Alqattan" <mansour.alqattan at gmail.com>
To: users at racket-lang.org
Sent: Wednesday, June 4, 2014 8:19:23 AM GMT -05:00 US/Canada Eastern
Subject: [racket] static analysis for finding vulnerabilities on non-executable and untyped language



Hello 


i am working on untyped intermediate programming language and this language is not meant to be for executing so it is non-executable. 


and it has already AST (Abstract Syntax Tree). 


I want only to find a method for doing static analysis on the coding to find the potential vulnerabilities i mean any vulnerabilities even if it is simple 


actually i am just learning about the static analysis, i would be grateful if you could help me with this 


thanks 


____________________
  Racket Users list:
  http://lists.racket-lang.org/users


Posted on the users mailing list.