Vulnerability Disclosure for Node.js Applications - CashCube and WEPL

This post is about two Server Side JS injection vulnerabilities that I found in CashCube, a node.js application which does personal money management and WEPL, a node.js based REPL.

In CashCube, the vulnerability is due to the use of unsanitized input in the eval command, this enables the attacker to pass arbitrary commands to the server. Can lead to shutdown of server or even deletion of files from the server filesystem. The details of the disclosure are on the github issue.

In WEPL, the vulnerability is due to a similar reason with the http request query parameter methodBody. The query parameter is directly passed to the eval function on the server side leading to possibility of command injection. The details of the disclosure are on the github issue. 

Executing OCaml Programs in Eclipse with OcaIDE

This blog post explains how to use OcaIDE to build and run your OCaml Programs. Assuming that you have installed OCaml, Eclipse and the OcaIDE plugin for OCaml, the first step is to setup the right paths to OCaml installation directory in the OcaIDE plugin configuration as shown in the below screenshots.

Once the path to the OCaml directory is set in eclipse you can create a new OCaml Project.The easiest way is to use the "OCaml Empty Makefile Project" type from the New Project Menu in Eclipse.

After creating a new project (say "lab03") right click it in the Navigator menu and click on import to add the files from the assignment in the new project.

Choose File System in the import menu to browse to the files downloaded from IVLE on your disk and check them to be added to this project.

Once you have added the files you can write your "Makefile" to build them. Right click the project and click New File as shown below.

Give the new file the name "Makefile" without any spaces or extension. Enter the following text in the file. The space after the "all:" line is a tab not a series of spaces. For more help about writing Makefile you can check the tutorial.

Once you have the Makefile in your project just right click it and select "Make Project". This would build the corresponding executable (lab03.exe here). If you get some errors make sure you gave the right path to the GNU Make installation in your system in the first step (e.g. C:\cygwin\bin\make.exe).

To execute the file just right click and choose  Run As "Ocaml Executable" as follows.

You should see some output on the console windows. If in the previous step you do not find any "Ocaml Executable" configuration click on the "Run Configurations..." menu item to create a new launch configuration.

Enter the name of the project and the choose the executable file to define a new launch configuration as shown above. Once you add the new configuration you can choose apply and run it. It should now execute with some output on the console window.

Life in Death

The truth of life is in death,
is this why our dreams are never met.
We go on with our lives everyday,
while the moment of truth is far away.

Life comes in its many shades,
while the blow of death is always gray.
Hopes are born with beginning of life,
death crushes them with no respite.

But is this really even life ?
filled with pain, sorrow, grief and spite.
When death is the only salvation,
why are we condemned to life's damnation.

Can you really repent your sins,
when you are bound by karma.
Will death be your salvation,
when in life you had no dharma.

Do you live to seek and find,
or to just go on with life's grind.
The seek ends at sundown with death,
when life cannot make further progress.

Death tests our regression into abyss,
filled with guilt and regret of life.
Do we really rise on the other side,
or death takes us for a long ride.

To live one must fight,
there is solace in last rite.
Does our fight go on beyond,
or does it end with the last yawn.

All our lives we move in different boxes,
the move always ends in the same casket.
Is death really the end of a move ?
or, on the other side, our journey begins anew.

When you see my cold dead eyes,
will you still care for the warmth of life ?
When the spirit leaves the humble abode,
does it travel a lonely road ?

We live all our lives divided by life,
while in death we all ultimately unite.
Is death then the only true god ?
when religions are filled with fright and fraud.

And what say we to this humble god,
not today, we are not ready to go abroad.
How long can we keep saying no ?
Does it even matter to all those in the know ?

The cycle of life and death goes on and on,
we come, we go, we shuffle around.
Life in death and death in life,
is there any difference, or, are they alike?

List Example for Extracting OCaml from Coq

In this post I will show how to extract a simple list append function written in Coq as OCaml code.

First let us create an inductive type in Coq to define our lists as follows.

Inductive mylist : Type :=

| nil : mylist 

| cons : nat -> mylist -> mylist.

Next, we will define an append function over these lists using the "Function" keyword.

Function myappend (l1:mylist) (l2:mylist) {struct l1} : mylist :=

match l1 with

| nil => l2

| cons x xs => cons x (myappend xs l2)

end.

The append function has a special "struct" which tells Coq that the first argument l1 is the recursive parameter to the function. This is essential as without that Coq will not let you define a function. In this particular case the recursive call is always made on a smaller list thus termination can be proven as an instance of structural recursion. However if we write a function where we want to use more general recursion we have to define a "measure" and prove that it decreases with every recursive call. Once the myappend function is defined in Coq it is easy to state and prove properties about append. The following theorem shows that myappend function is associative. 

Theorem myappend_assoc : forall l1 l2 l3 : mylist , myappend (myappend l1 l2) l3 =

(myappend l1 (myappend l2 l3)).

Proof.

intros.

induction l1.

simpl.

trivial.

simpl.

rewrite IHl1.

trivial.

Qed.

Once we have stated the desired properties and proven their correctness we can also generate OCaml (or Haskell) code from Coq using extraction process. The extraction process will recursively remove the proof terms from the code and convert the program to a corresponding OCaml program. Extraction for the myappend function can be using the following statements in Coq.

Extraction Language Ocaml.

Extraction "mylist.ml" myappend.

The generated code in mylist.ml file looks as below.

type nat =

| O

| S of nat

type mylist =

| Nil

| Cons of nat * mylist

(** val myappend : mylist -> mylist -> mylist **)

let rec myappend l1 l2 =

match l1 with

| Nil -> l2

| Cons (x, xs) -> Cons (x, (myappend xs l2))

The OCaml code extracted from Coq includes all the corresponding data types - nat and mylist used in the program. Also the function myappend is extracted without the proof of termination. Other proof constructs like theorems are also dropped from the extracted code. The extracted code can now be used inside a larger OCaml program.