Skip to content

Commit c933b0e

Browse files
marek-trtikmarek-trtik
authored
Merge pull request diffblue#170 from diffblue/feature/cmdline_option_old_instrumenter
SEC-5: Introducing a command-line option --use-old-instrumentation.
2 parents 42dfc44 + d2e6fda commit c933b0e

15 files changed

+49
-41
lines changed

‎benchmarks/TRAINING/diffblue/taint_traces_01_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎benchmarks/TRAINING/diffblue/taint_traces_02_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎benchmarks/TRAINING/diffblue/taint_traces_03_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎benchmarks/TRAINING/diffblue/taint_traces_04_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎benchmarks/TRAINING/diffblue/taint_traces_05_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎benchmarks/TRAINING/diffblue/taint_traces_06_evaluator.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
"category": "TRAINING",
99
"source": "DiffBlue",
1010
"installer": "__benchmark_installer_TRAINING_diffblue",
11-
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program",
11+
"custom-options-for-security-scanner": "--rebuild --verbosity 0 --dump-html-summaries --dump-html-statistics --dump-html-slice --dump-html-program --data-flow-insensitive-instrumentation",
1212
"expected-results":
1313
{
1414
"error-traces-json": "search_for_error_traces/error_traces.json",

‎security-scanner/analyser.py

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ def run_security_analyser(
2929
dump_html_slice,
3030
dump_html_program,
3131
verbosity,
32+
data_flow_insensitive_instrumentation,
3233
results_dir,
3334
temp_root_dir
3435
):
@@ -55,7 +56,8 @@ def run_security_analyser(
5556
"timeout": timeout,
5657
"verbosity": verbosity,
5758
"output-dir": "./",
58-
"temp-dir": os.path.relpath(temp_root_dir,results_dir)
59+
"temp-dir": os.path.relpath(temp_root_dir,results_dir),
60+
"data-flow-insensitive-instrumentation": data_flow_insensitive_instrumentation
5961
}
6062
if dump_html_summaries:
6163
root_config_json["dump_html_summaries"] = True

‎security-scanner/run.py

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,13 @@ def __parse_cmd_line():
5757
parser.add_argument("--verbosity", type=int, default=9,
5858
help="It specifies how many debugging messages will be printed to the standard output stream "
5959
"during the analysis.")
60+
parser.add_argument("--data-flow-insensitive-instrumentation", action="store_true",
61+
help="If specified, then the tool 'security-analyser' will use the data-flow insensitive "
62+
"instrumentation of the checked properties into the output GOTO programs. In that case"
63+
"the propagation of taint information will only be control-flow sensitive. The advantage "
64+
"of this data-flow insensitive instrumentation is that it allows more aggressive program "
65+
"slicing and so smaller programs for CBMC to analyse, i.e. considerably faster analysis. "
66+
"The disadvantage is that some of the generated error traces might be false positives.")
6067
return parser.parse_args()
6168

6269

@@ -97,6 +104,7 @@ def evaluate(cmdline):
97104
cmdline.dump_html_slice,
98105
cmdline.dump_html_program,
99106
cmdline.verbosity,
107+
cmdline.data_flow_insensitive_instrumentation,
100108
cmdline.results_dir,
101109
os.path.abspath(os.path.join(cmdline.temp_dir,"GOTO-ANALYSER-TEMP"))
102110
)

‎src/taint-analysis/taint_config.cpp

Lines changed: 7 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ taint_configt::taint_configt(const std::string &cfg_fname)
2121
, dump_html_statistics(false)
2222
, dump_html_slice(false)
2323
, dump_html_program(false)
24+
, data_flow_insensitive_instrumentation(false)
2425
{
2526
}
2627

@@ -196,34 +197,12 @@ bool taint_configt::load(message_handlert &handler)
196197
verbosity=std::atoi(attr_it->second.value.c_str());
197198
}
198199

199-
{
200-
auto attr_it=cfg.object.find("dump_html_summaries");
201-
if (attr_it==cfg.object.cend())
202-
dump_html_summaries=false;
203-
else
204-
dump_html_summaries=attr_it->second.is_true();
205-
}
206-
{
207-
auto attr_it=cfg.object.find("dump_html_statistics");
208-
if (attr_it==cfg.object.cend())
209-
dump_html_statistics=false;
210-
else
211-
dump_html_statistics=attr_it->second.is_true();
212-
}
213-
{
214-
auto attr_it=cfg.object.find("dump_html_slice");
215-
if (attr_it==cfg.object.cend())
216-
dump_html_slice=false;
217-
else
218-
dump_html_slice=attr_it->second.is_true();
219-
}
220-
{
221-
auto attr_it=cfg.object.find("dump_html_program");
222-
if (attr_it==cfg.object.cend())
223-
dump_html_program=false;
224-
else
225-
dump_html_program=attr_it->second.is_true();
226-
}
200+
dump_html_summaries=cfg["dump_html_summaries"].is_true();
201+
dump_html_statistics=cfg["dump_html_statistics"].is_true();
202+
dump_html_slice=cfg["dump_html_slice"].is_true();
203+
dump_html_program=cfg["dump_html_program"].is_true();
204+
data_flow_insensitive_instrumentation=
205+
cfg["data-flow-insensitive-instrumentation"].is_true();
227206

228207
return false;
229208
}

‎src/taint-analysis/taint_config.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,11 @@ class taint_configt
9595
return dump_html_program;
9696
}
9797

98+
bool use_data_flow_insensitive_instrumentation() const
99+
{
100+
return data_flow_insensitive_instrumentation;
101+
}
102+
98103
private:
99104
taint_configt() = delete;
100105
taint_configt(const taint_configt &) = delete;
@@ -115,6 +120,7 @@ class taint_configt
115120
bool dump_html_statistics;
116121
bool dump_html_slice;
117122
bool dump_html_program;
123+
bool data_flow_insensitive_instrumentation;
118124
};
119125

120126

‎src/taint-analysis/taint_security_scanner.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ bool taint_do_security_scan(
178178
"SLICER"),
179179
&statistics,
180180
&logger);
181-
slicer.compute_slice();
181+
slicer.compute_slice(config.use_data_flow_insensitive_instrumentation());
182182
}
183183

184184
if(config.is_html_dump_of_program_slice_enabled())

‎src/taint-slicer/instrumenter.cpp

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,10 +41,17 @@ static std::string generate_fresh_automaton_variable_for_token(
4141
taint_instrumentert::taint_instrumentert(
4242
const taint_instrumentation_propst &props,
4343
const taint_programt *const in_program,
44-
taint_statisticst *const in_statistics)
44+
taint_statisticst *const in_statistics,
45+
const bool use_data_flow_insensitive_instrumentation)
4546
: program(in_program)
4647
, statistics(in_statistics)
48+
, use_data_flow_insensitive_version(use_data_flow_insensitive_instrumentation)
4749
{
50+
// The next line must be here in order to prevent clang produce the error:
51+
// `error: private field 'use_data_flow_insensitive_version' is not used
52+
// [-Werror,-Wunused-private-field]`
53+
(void)use_data_flow_insensitive_version;
54+
4855
assert(program!=nullptr);
4956
assert(statistics!=nullptr);
5057

‎src/taint-slicer/instrumenter.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,8 @@ class taint_instrumentert
5252
taint_instrumentert(
5353
const taint_instrumentation_propst &props,
5454
const taint_programt * const in_program,
55-
taint_statisticst * const in_statistics);
55+
taint_statisticst * const in_statistics,
56+
const bool use_data_flow_insensitive_instrumentation);
5657

5758
const goto_functionst &get_instrumented_functions() const
5859
{ return instrumented_functions; }
@@ -92,6 +93,7 @@ class taint_instrumentert
9293
symbol_tablet instrumented_symbol_table;
9394
std::map<taint_tokent::namet, automaton_variable_idt>
9495
from_tokens_to_vars;
96+
bool use_data_flow_insensitive_version;
9597
};
9698

9799
typedef taint_instrumentert::automaton_variable_idt

‎src/taint-slicer/slicer.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,8 @@ taint_slicert::taint_slicert(
4242
fileutl_create_directory(this->temp_dir);
4343
}
4444

45-
void taint_slicert::compute_slice()
45+
void taint_slicert::compute_slice(
46+
const bool use_data_flow_insensitive_instrumentation)
4647
{
4748
taint_map_from_rules_to_their_application_sitest
4849
map_from_functions_to_rule_application_sites;
@@ -97,7 +98,10 @@ void taint_slicert::compute_slice()
9798
for(std::size_t i=0UL, n=instrumentation_props.size(); i!=n; ++i)
9899
{
99100
const taint_instrumentert instrumenter(
100-
instrumentation_props.at(i),program,statistics);
101+
instrumentation_props.at(i),
102+
program,
103+
statistics,
104+
use_data_flow_insensitive_instrumentation);
101105
const std::pair<taint_slicing_taskt,std::string> task_valid=
102106
build_slicing_task(
103107
instrumentation_props.at(i),

‎src/taint-slicer/slicer.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ class taint_slicert
4848
propagation graph (see member @tokens_propagation_graph).
4949
5050
\*******************************************************************/
51-
void compute_slice();
51+
void compute_slice(const bool use_data_flow_insensitive_instrumentation);
5252

5353
private:
5454
taint_slicert(const taint_slicert &)=delete;

0 commit comments

Comments
 (0)