Commit a8b038ab authored by Joachim Müssig's avatar Joachim Müssig

add two insecure examples

parent 584aadd2
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/ObjectSensLeak",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/program.jar",
pathToJavaFile : "program/",
pathToSDG : "SDG/ObjectSensLeak.pdg",
entryMethod : "ObjectSensLeak",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/ObjectSensLeak.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int ObjectSensLeak.callTest(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int ObjectSensLeak.callTest(int, int):5) return v5"}}]
\ No newline at end of file
directoryPath : "/home/joachim/JoanaKeYBeispiele/SecureExamples/ObjectSensLeak",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/program.jar",
pathToJavaFile : "program/",
pathToSDG : "SDG/ObjectSensLeak.pdg",
entryMethod : "ObjectSensLeak",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/ObjectSensLeak.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "59", sdgNode : "ObjectSensLeak.callTest(II)I -> param 1 FRMI"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "57", sdgNode : "ObjectSensLeak.callTest(II)I -> ObjectSensLeak.callTest(int,int) EXIT"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 114, "cg_node" : {"id" : 5, "cg_node_id" :13, "ir" : {
}}},
{ "sdg_node" : 99, "cg_node" : {"id" : 4, "cg_node_id" :12, "ir" : {
}}},
{ "sdg_node" : 100, "cg_node" : {"id" : 4, "cg_node_id" :12, "ir" : {
}}},
{ "sdg_node" : 142, "cg_node" : {"id" : 5, "cg_node_id" :13, "ir" : {
}}},
],
"cg_nodes" : [
{"id" : 0, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 1, "cg_node_id" :0, "ir" : {
}},
{"id" : 2, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 3, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 4, "cg_node_id" :12, "ir" : {
}},
{"id" : 5, "cg_node_id" :13, "ir" : {
}},
],
"localPointerKeys" : [{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
{"id" : 4, "value_number" : 1, "node" : 4
},
{"id" : 5, "value_number" : 1, "node" : 5
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 44, "cg_node" : 6},
{ "sdg_node" : 111, "cg_node" : 13},
{ "sdg_node" : 18, "cg_node" : 0},
{ "sdg_node" : 35, "cg_node" : 1},
{ "sdg_node" : 56, "cg_node" : 9},
{ "sdg_node" : 124, "cg_node" : 14},
{ "sdg_node" : 96, "cg_node" : 12},
{ "sdg_node" : 1, "cg_node" : 5},
{ "sdg_node" : 69, "cg_node" : 11},
],
"nodeToSSA" : [{ "sdg_node" : 104, "iIndex" : 4},
{ "sdg_node" : 122, "iIndex" : 3},
{ "sdg_node" : 88, "iIndex" : 12},
{ "sdg_node" : 84, "iIndex" : 11},
{ "sdg_node" : 105, "iIndex" : 4},
{ "sdg_node" : 106, "iIndex" : 4},
{ "sdg_node" : 80, "iIndex" : 8},
{ "sdg_node" : 79, "iIndex" : 5},
{ "sdg_node" : 75, "iIndex" : 3},
{ "sdg_node" : 74, "iIndex" : 0},
{ "sdg_node" : 118, "iIndex" : 2},
{ "sdg_node" : 66, "iIndex" : 3},
{ "sdg_node" : 61, "iIndex" : 2},
{ "sdg_node" : 51, "iIndex" : 4},
{ "sdg_node" : 50, "iIndex" : 3},
{ "sdg_node" : 49, "iIndex" : 3},
{ "sdg_node" : 48, "iIndex" : 1},
{ "sdg_node" : 47, "iIndex" : 1},
{ "sdg_node" : 42, "iIndex" : 2},
{ "sdg_node" : 40, "iIndex" : 1},
{ "sdg_node" : 38, "iIndex" : 0},
{ "sdg_node" : 32, "iIndex" : 5},
{ "sdg_node" : 128, "iIndex" : 1},
{ "sdg_node" : 29, "iIndex" : 4},
{ "sdg_node" : 28, "iIndex" : 3},
{ "sdg_node" : 27, "iIndex" : 3},
{ "sdg_node" : 26, "iIndex" : 3},
{ "sdg_node" : 25, "iIndex" : 3},
{ "sdg_node" : 24, "iIndex" : 2},
{ "sdg_node" : 23, "iIndex" : 1},
{ "sdg_node" : 21, "iIndex" : 0},
{ "sdg_node" : 117, "iIndex" : 1},
{ "sdg_node" : 116, "iIndex" : 1},
{ "sdg_node" : 115, "iIndex" : 1},
{ "sdg_node" : 14, "iIndex" : 4},
{ "sdg_node" : 107, "iIndex" : 5},
{ "sdg_node" : 9, "iIndex" : 2},
{ "sdg_node" : 8, "iIndex" : 1},
{ "sdg_node" : 7, "iIndex" : 1},
{ "sdg_node" : 6, "iIndex" : 0},
{ "sdg_node" : 5, "iIndex" : 0},
{ "sdg_node" : 101, "iIndex" : 1},
]
}
\ No newline at end of file
public class A
{
private int i ;
public A ( int i )
{
this . i = i ;
}
public int doPrint ( )
{
return out ( this . i ) ;
}
public static int out ( int i )
{
return i ;
}
}
public class ObjectSensLeak
{
public static int high = 0 ;
public static int low = 1 ;
public static void main ( String [ ] args )
{
callTest ( high , low ) ;
}
public static int callTest ( int high , int low )
{
return test ( high , low ) ;
}
public static int test ( int h , int l )
{
A a1 = new A ( l ) ;
A a2 = new A ( h ) ;
return a1 . doPrint ( ) ;
}
}
public class A
{
private int i ;
public A ( int i )
{
this . i = i ;
}
public int doPrint ( )
{
return out ( this . i ) ;
}
public static int out ( int i )
{
return i ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class ObjectSensLeak
{
public static int high = 0 ;
public static int low = 1 ;
public static void main ( String [ ] args )
{
callTest ( high , low ) ;
}
public static int callTest ( int high , int low )
{
return test ( high , low ) ;
}
public static int test ( int h , int l )
{
A a1 = new A ( l ) ;
A a2 = new A ( h ) ;
return a1 . doPrint ( ) ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class A
{
private int i ;
public A ( int i )
{
this . i = i ;
}
public int doPrint ( )
{
return out ( this . i ) ;
}
public static int out ( int i )
{
return i ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class ObjectSensLeak
{
//sliced: public static int high = 0 ;
public static int low = 1 ;
public static void main ( String [ ] args )
{
callTest ( high , low ) ;
}
public static int callTest ( int high , int low )
{
return test ( high , low ) ;
}
public static int test ( int h , int l )
{
A a1 = new A ( l ) ;
A a2 = new A ( h ) ;
return a1 . doPrint ( ) ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program/testdata/build/src.jar",
pathToJavaFile : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program/src/",
pathToSDG : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program/SDG/Program.pdg",
entryMethod : "Program",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program/SDG/Program.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "50", sdgNode : "Program.callFoo(I)I -> param 1 <param> 1"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "56", sdgNode : "Program.callFoo(I)I -> return v5 Program.callFoo(I)I"}}]
\ No newline at end of file
directoryPath : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/Program.pdg",
entryMethod : "Program",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/Program.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int Program.callFoo(int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int Program.callFoo(int):5) return v5"}}]
\ No newline at end of file
directoryPath : "/home/joachim/JoanaKeYBeispiele/InsecureExample/Array2/program",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/Program.pdg",
entryMethod : "Program",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/Program.dispro",
sources : [{securityLevel : "high", description : {from : "sdgNode", sdgNodeId : "50", sdgNode : "Program.callFoo(I)I -> param 1 FRMI"}}],
sinks : [{securityLevel : "low", description : {from : "sdgNode", sdgNodeId : "47", sdgNode : "Program.callFoo(I)I -> Program.callFoo(int) EXIT"}}]
\ No newline at end of file
This diff is collapsed.
{"formal_ins_to_pers_cg" : [
{ "sdg_node" : 49, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {
}}},
{ "sdg_node" : 50, "cg_node" : {"id" : 4, "cg_node_id" :9, "ir" : {
}}},
{ "sdg_node" : 40, "cg_node" : {"id" : 3, "cg_node_id" :8, "ir" : {
}}},
{ "sdg_node" : 63, "cg_node" : {"id" : 6, "cg_node_id" :11, "ir" : {
}}},
],
"cg_nodes" : [
{"id" : 0, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 1, "cg_node_id" :0, "ir" : {
}},
{"id" : 2, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 3, "cg_node_id" :8, "ir" : {
}},
{"id" : 4, "cg_node_id" :9, "ir" : {
}},
{"id" : 5, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 6, "cg_node_id" :11, "ir" : {
}},
],
"localPointerKeys" : [{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
{"id" : 4, "value_number" : 1, "node" : 4
},
{"id" : 5, "value_number" : 1, "node" : 5
},
{"id" : 6, "value_number" : 1, "node" : 6
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 20, "cg_node" : 0},
{ "sdg_node" : 37, "cg_node" : 8},
{ "sdg_node" : 59, "cg_node" : 11},
{ "sdg_node" : 1, "cg_node" : 5},
{ "sdg_node" : 46, "cg_node" : 9},
],
"nodeToSSA" : [{ "sdg_node" : 44, "iIndex" : 2},
{ "sdg_node" : 41, "iIndex" : 1},
{ "sdg_node" : 34, "iIndex" : 5},
{ "sdg_node" : 56, "iIndex" : 3},
{ "sdg_node" : 31, "iIndex" : 4},
{ "sdg_node" : 30, "iIndex" : 3},
{ "sdg_node" : 29, "iIndex" : 3},
{ "sdg_node" : 28, "iIndex" : 3},
{ "sdg_node" : 27, "iIndex" : 3},
{ "sdg_node" : 26, "iIndex" : 2},
{ "sdg_node" : 25, "iIndex" : 1},
{ "sdg_node" : 23, "iIndex" : 0},
{ "sdg_node" : 69, "iIndex" : 6},
{ "sdg_node" : 68, "iIndex" : 5},
{ "sdg_node" : 67, "iIndex" : 5},
{ "sdg_node" : 66, "iIndex" : 5},
{ "sdg_node" : 65, "iIndex" : 5},
{ "sdg_node" : 64, "iIndex" : 1},
{ "sdg_node" : 14, "iIndex" : 8},
{ "sdg_node" : 9, "iIndex" : 6},
{ "sdg_node" : 6, "iIndex" : 2},
{ "sdg_node" : 5, "iIndex" : 0},
{ "sdg_node" : 51, "iIndex" : 2},
]
}
\ No newline at end of file
This diff is collapsed.
public class Program
{
public static void main ( String [ ] args )
{
Program p = new Program ( ) ;
p . callFoo ( 14 ) ;
}
public int callFoo ( int h )
{
return foo ( h ) ;
}
public int foo ( int h )
{
int [ ] a = new int [ h ] ;
return a [ 5 ] ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class Program
{
public static void main ( String [ ] args )
{
Program p = new Program ( ) ;
p . callFoo ( 14 ) ;
}
public int callFoo ( int h )
{
return foo ( h ) ;
}
public int foo ( int h )
{
int [ ] a = new int [ h ] ;
return a [ 5 ] ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
public class Program
{
public static void main ( String [ ] args )
{
Program p = new Program ( ) ;
p . callFoo ( 14 ) ;
}
public int callFoo ( int h )
{
return foo ( h ) ;
}
public int foo ( int h )
{
int [ ] a = new int [ h ] ;
return a [ 5 ] ;
}
}
directoryPath : "/home/joachim/JoanaKeYBeispiele/InsecureExample/divideByZero",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/program.jar",
pathToJavaFile : "program/",
pathToSDG : "SDG/DivisionByZero.pdg",
entryMethod : "DivisionByZero",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/DivisionByZero.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 2 of method int DivisionByZero.callDivide(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "(int DivisionByZero.callDivide(int, int):5) return v5"}}]
\ No newline at end of file
{"formal_ins_to_pers_cg" : [
],
"cg_nodes" : [
{"id" : 0, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 1, "cg_node_id" :0, "ir" : {
}},
{"id" : 2, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
{"id" : 3, "cg_node_id" :0, "ir" : {
"1" : "this"
}},
],
"localPointerKeys" : [{"id" : 0, "value_number" : 1, "node" : 0
},
{"id" : 1, "value_number" : 1, "node" : 1
},
{"id" : 2, "value_number" : 1, "node" : 2
},
{"id" : 3, "value_number" : 1, "node" : 3
},
],
"disjunctPointsTo" : [],
"entryNodesToCG" : [{ "sdg_node" : 18, "cg_node" : 0},
{ "sdg_node" : 40, "cg_node" : 9},
{ "sdg_node" : 35, "cg_node" : 8},
{ "sdg_node" : 53, "cg_node" : 11},
{ "sdg_node" : 1, "cg_node" : 5},
],
"nodeToSSA" : [{ "sdg_node" : 45, "iIndex" : 2},
{ "sdg_node" : 58, "iIndex" : 4},
{ "sdg_node" : 38, "iIndex" : 1},
{ "sdg_node" : 32, "iIndex" : 5},
{ "sdg_node" : 29, "iIndex" : 4},
{ "sdg_node" : 28, "iIndex" : 3},
{ "sdg_node" : 27, "iIndex" : 3},
{ "sdg_node" : 26, "iIndex" : 3},
{ "sdg_node" : 25, "iIndex" : 3},
{ "sdg_node" : 24, "iIndex" : 2},
{ "sdg_node" : 23, "iIndex" : 1},
{ "sdg_node" : 21, "iIndex" : 0},
{ "sdg_node" : 16, "iIndex" : 4},
{ "sdg_node" : 62, "iIndex" : 11},
{ "sdg_node" : 61, "iIndex" : 9},
{ "sdg_node" : 59, "iIndex" : 6},
{ "sdg_node" : 11, "iIndex" : 2},
{ "sdg_node" : 8, "iIndex" : 1},
{ "sdg_node" : 5, "iIndex" : 0},
{ "sdg_node" : 50, "iIndex" : 3},
]
}
\ No newline at end of file
This diff is collapsed.
import java . lang . ArithmeticException ;
public class DivisionByZero
{
public static int divide ( int l , int h )
{
int z = 0 ;
try
{
z = l / h ;
}
catch ( ArithmeticException e )
{
return h ;
}
return z ;
}
public static int callDivide ( int l , int h )
{
return divide ( l , h ) ;
}
public static void main ( String [ ] args )
{
callDivide ( randInt ( ) , randInt ( ) ) ;
}
static int randInt ( )
{
return 42 ;
}
}
import java . lang . ArithmeticException ;
public class DivisionByZero
{
public static int divide ( int l , int h )
{
int z = 0 ;
try
{
z = l / h ;
}
catch ( ArithmeticException e )
{
return h ;
}
return z ;
}
public static int callDivide ( int l , int h )
{
return divide ( l , h ) ;
}
public static void main ( String [ ] args )
{
callDivide ( randInt ( ) , randInt ( ) ) ;
}
static int randInt ( )
{
return 42 ;
}
/*@
@ requires true;
@ ensures b;
@*/
private void assume(boolean b) {
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!