Nusmv逆向分析

Nusmv逆向分析

LTL model checkers根据其原理可分为explicit和symbolic两类，前一类如SPIN的基本原理是显式地构建系统的状态空间，再搜索违背给定性质的迹，后者如NuSMV的基本原理是以符号化的方式表征系统模型，使用二分决策图（Binary Decision Diagram）来分析模型

LTL satisfiability checking的基本理论思路可分为四个步骤（资料来源于这本著作：Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press.）

表征系统的状态空间，通常用Kripke结构
将给定的LTL性质转变为其否定形式所等价的buchi自动机
将得到的Kripke结构和buchi自动机结合得到一个迁移系统
查看该迁移系统是否存在一条由初始状态导出的路径，如果存在则意味着原有系统中存在一条迹违背了给定的LTL性质，如果不存在这样的路径则意味着系统具有给定的LTL性质
所以State2.1是初始状态而不是部分状态
init(homePresentState):= not_present;
init(alarmState):= off;
init(各种delay):= 0;

循环次数造成 ×
check时造成
trace时造成

动态调试配置

首先load library，因为勾选了所以会停住，thread start也会停住

IDA分析

– as demonstrated by the following execution sequence
依次交叉引用

__int64 __fastcall Mc_CheckCTLSpec(__int64 a1,__int64 a2)
__int64 __fastcall Bmc_Utils_generate_and_print_cntexample(int a1, __int64 a2, __int64 a3, __int64 a4, int a5, __int64 a6, __int64 a7)
__int64 __fastcall Bmc_GenSolveInvar(__int64 a1, __int64 a2, char a3, int a4, char *Source)	/	__int64 __fastcall Bmc_GenSolveInvar_EenSorensson(__int64 a1, __int64 a2, int a3, int a4, char *Source, char a6)
__int64 __fastcall Ltl_StructCheckLtlSpec_explain(__int64 a1, __int64 a2)	/	__int64 __fastcall Ltl_CheckLtlSpec(__int64 a1, __int64 a2)
__int64 __fastcall Mc_CheckAGOnlySpec(__int64 a1, __int64 a2)
__int64 __fastcall print_result(__int64 a1, __int64 a2)
__int64 __fastcall Sbmc_Utils_generate_and_print_cntexample(__int64 a1, __int64 a2, int a3, int a4, int a5, __int64 a6, __int64 a7)                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             

在每处都下断点

NuSMVCore_main -> get_tool_version(main)、mingw_fprintf–>Cmd_CommandExecute(main，输错指令就跳出)

发现
check_ctlspec -p "AG (alarm.alarmCap.alarm=siren -> AF (runinfan61.timer=2 & fan.switchCap.switch = on))"在 Mc_CheckCTLSpec里的回显处停下

print_output 对应 – as demonstrated by the following execution sequence

call _TraceMgr_execute_plugin 输出路径

_CommandSource->_Cmd_CommandExecute->_com_dispatch->_CommandCheckCtlSpec->prop_verify->Mc_CheckCTLSpec
_CommandSource中的call _CmdFgetsFilec叫下一次

关键函数

_opt_counter_examples?_BddEnc_pick_one_state? _Mc_create_trace_from_bdd_state_input_list?_TraceMgr_register_trace?
bdd指的是BDD算法

源码位置

NuSMV-2.6.0 (1)NuSMV-2.6.0NuSMVcodenusmvcorepropProp.c

void prop_verify(Prop_ptr self)
{const NuSMVEnv_ptr env = ENV_OBJECT(self)->environment;const ErrorMgr_ptr errmgr =ERROR_MGR(NuSMVEnv_get_value(env, ENV_ERROR_MANAGER));const OptsHandler_ptr opts =OPTS_HANDLER(NuSMVEnv_get_value(env, ENV_OPTS_HANDLER));if (Prop_get_status(self) == Prop_Unchecked)  {switch (Prop_get_type(self)) {case Prop_Ctl:if (opt_ag_only(opts)) {if ( opt_forward_search(opts)) { Mc_CheckAGOnlySpec(env, self); }else {/* Cannot use AG-only since reachables must be calculated before */ErrorMgr_warning_ag_only_without_reachables(errmgr);Mc_CheckCTLSpec(env, self);}}else { Mc_CheckCTLSpec(env, self); }break;case Prop_Compute:  Mc_CheckCompute(env, self); break;case Prop_Invar:    Mc_CheckInvar(env, self); break;case Prop_Ltl:      Ltl_CheckLtlSpec(env, self); break;case Prop_Psl:if (Prop_is_psl_ltl(self)) { Ltl_CheckLtlSpec(env, self); }else {if (Prop_is_psl_obe(self)) {if (opt_ag_only(opts)) {if ( opt_forward_search(opts)) { Mc_CheckAGOnlySpec(env, self); }else {/* Cannot use AG-only since reachables must be calculated before */ErrorMgr_warning_ag_only_without_reachables(errmgr);Mc_CheckCTLSpec(env, self);}}else { Mc_CheckCTLSpec(env, self); }}else { ErrorMgr_error_psl_not_supported_feature(errmgr); }}break;default:  error_unreachable_code(); /* invalid type */}}
}

NuSMV-2.6.0 (1)NuSMV-2.6.0NuSMVcodenusmvcoremcmcMC.c

void Mc_CheckCTLSpec(NuSMVEnv_ptr env, Prop_ptr prop)
{const StreamMgr_ptr streams =STREAM_MGR(NuSMVEnv_get_value(env, ENV_STREAM_MANAGER));const ErrorMgr_ptr errmgr =ERROR_MGR(NuSMVEnv_get_value(env, ENV_ERROR_MANAGER));node_ptr exp;Trace_ptr trace;bdd_ptr s0, tmp_1, tmp_2;BddFsm_ptr fsm;BddEnc_ptr enc;DDMgr_ptr dd;Expr_ptr spec  = Prop_get_expr_core(prop);const OptsHandler_ptr opts =OPTS_HANDLER(NuSMVEnv_get_value(env, ENV_OPTS_HANDLER));const NodeMgr_ptr nodemgr =NODE_MGR(NuSMVEnv_get_value(env, ENV_NODE_MGR));if (opt_verbose_level_gt(opts, 0)) {Logger_ptr logger = LOGGER(NuSMVEnv_get_value(env, ENV_LOGGER));Logger_log(logger, "evaluating ");print_spec(Logger_get_ostream(logger), prop, get_prop_print_method(opts));Logger_log(logger, "n");}fsm = Prop_compute_ground_bdd_fsm(env, prop);enc = BddFsm_get_bdd_encoding(fsm);dd = BddEnc_get_dd_manager(enc);/* Evaluates the spec */s0 = eval_ctl_spec(fsm, enc, spec, Nil);tmp_1 = bdd_not(dd, s0);tmp_2 = BddFsm_get_state_constraints(fsm);bdd_and_accumulate(dd, &tmp_2 , tmp_1);bdd_free(dd, tmp_1);tmp_1 = BddFsm_get_fair_states(fsm);if (bdd_is_false(dd, tmp_1)) {ErrorMgr_warning_fsm_fairness_empty(errmgr);}bdd_and_accumulate(dd, &tmp_2 , tmp_1);bdd_free(dd, tmp_1);bdd_free(dd, s0);s0 = BddFsm_get_init(fsm);bdd_and_accumulate(dd, &s0, tmp_2);bdd_free(dd, tmp_2);/* Prints out the result, if not true explain. */StreamMgr_print_output(streams,  "-- ");print_spec(StreamMgr_get_output_ostream(streams),prop, get_prop_print_method(opts));if (bdd_is_false(dd, s0)) {StreamMgr_print_output(streams,  "is truen");Prop_set_status(prop, Prop_True);}else {StreamMgr_print_output(streams,  "is falsen");Prop_set_status(prop, Prop_False);if (opt_counter_examples(opts)) {char* trace_title = NULL;char* trace_title_postfix = " Counterexample";tmp_1 = BddEnc_pick_one_state(enc, s0);bdd_free(dd, s0);s0 = bdd_dup(tmp_1);bdd_free(dd, tmp_1);exp = reverse(explain(fsm, enc, cons(nodemgr, (node_ptr) bdd_dup(s0), Nil),spec, Nil));if (exp == Nil) {/* The counterexample consists of one initial state */exp = cons(nodemgr, (node_ptr) bdd_dup(s0), Nil);}/* The trace title depends on the property type. For example itis in the form "LTL Counterexample" */trace_title = ALLOC(char,strlen(Prop_get_type_as_string(prop)) +strlen(trace_title_postfix) + 1);nusmv_assert(trace_title != (char*) NULL);strcpy(trace_title, Prop_get_type_as_string(prop));strcat(trace_title, trace_title_postfix);{SexpFsm_ptr sexp_fsm; /* needed for trace lanugage */sexp_fsm = Prop_get_scalar_sexp_fsm(prop);if (SEXP_FSM(NULL) == sexp_fsm) {sexp_fsm = SEXP_FSM(NuSMVEnv_get_value(env, ENV_SEXP_FSM));SEXP_FSM_CHECK_INSTANCE(sexp_fsm);}trace = Mc_create_trace_from_bdd_state_input_list(enc,SexpFsm_get_symbols_list(sexp_fsm), trace_title,TRACE_TYPE_CNTEXAMPLE, exp);}FREE(trace_title);StreamMgr_print_output(streams, "-- as demonstrated by the following execution sequencen");TraceMgr_register_trace(TRACE_MGR(NuSMVEnv_get_value(env, ENV_TRACE_MGR)), trace);//////TraceMgr_execute_plugin(TRACE_MGR(NuSMVEnv_get_value(env, ENV_TRACE_MGR)), TRACE_OPT(NULL),TRACE_MGR_DEFAULT_PLUGIN,TRACE_MGR_LAST_TRACE);Prop_set_trace(prop, Trace_get_id(trace));walk_dd(dd, bdd_free, exp);free_list(nodemgr, exp);}}bdd_free(dd, s0);
} /* Mc_CheckCTLSpec */

fsm = Prop_compute_ground_bdd_fsm(env, prop);
enc = BddFsm_get_bdd_encoding(fsm);
dd = BddEnc_get_dd_manager(enc);
s0 = eval_ctl_spec(fsm, enc, spec, Nil);
s0 = BddFsm_get_init(fsm);

    trace = Mc_create_trace_from_bdd_state_input_list(enc,SexpFsm_get_symbols_list(sexp_fsm), trace_title,TRACE_TYPE_CNTEXAMPLE, exp);

sexp_fsm = Prop_get_scalar_sexp_fsm(prop); prop
exp = reverse(explain(fsm, enc, cons(nodemgr, (node_ptr) bdd_dup(s0), Nil),
spec, Nil));
enc经过分析没变 sexp_fsm = Prop_get_scalar_sexp_fsm(prop); prop没变 exp没变，但是对应地址的内容变没变还不知道 ，应该是读取了enc里的状态
v14 = NuSMVEnv_get_value(a1, “+4_trace_mgr”);
TraceMgr_execute_plugin(v14, 0, -1, -1);

dd 有没有变化?没有
s0有没有变化？

void Mc_CheckCTLSpec(NuSMVEnv_ptr env, Prop_ptr prop)

NuSMV-2.6.0 (1)NuSMV-2.6.0NuSMVcodenusmvcoremcmcTrace.c

Trace_ptr Mc_create_trace_from_bdd_state_input_list(const BddEnc_ptr bdd_enc,const NodeList_ptr symbols,const char* desc,const TraceType type,node_ptr path)
{Trace_ptr trace;if (Nil == path) return TRACE(NULL);trace = Trace_create(BaseEnc_get_symb_table(BASE_ENC(bdd_enc)),desc, type, symbols, false);return Mc_fill_trace_from_bdd_state_input_list(bdd_enc, trace, path);
}Trace_ptr Mc_fill_trace_from_bdd_state_input_list(const BddEnc_ptr bdd_enc,Trace_ptr trace,node_ptr path)
{TraceIter step;NodeList_ptr sf_vars;NodeList_ptr i_vars;#if MC_MODEL_DEBUGint i = 1; /* for debugging only */
#endifnusmv_assert(Nil != path);TRACE_CHECK_INSTANCE(trace);nusmv_assert(Trace_is_empty(trace));sf_vars = Trace_get_sf_vars(trace);i_vars = Trace_get_i_vars(trace);step = Trace_first_iter(trace);#if MC_MODEL_DEBUGStreamMgr_print_error(streams,  "n--- MC Model extraction ---n");
#endif/* first node of path is initial state */mc_trace_step_put_values(trace, step, bdd_enc, BDD_STATES(car(path)), sf_vars);#if MC_MODEL_DEBUGmc_model_trace_step_print(trace, step, TRACE_ITER_SF_VARS, "S", i);
#endifpath = cdr(path);while (path != Nil) {/* append one more (i,S) to trace */step = Trace_append_step(trace);mc_trace_step_put_values(trace, step, bdd_enc, BDD_INPUTS(car(path)), i_vars);#if MC_MODEL_DEBUGmc_model_trace_step_print(trace, step, TRACE_ITER_I_VARS, "I", ++ i);
#endifpath = cdr(path); nusmv_assert(Nil != path);mc_trace_step_put_values(trace, step, bdd_enc, BDD_STATES(car(path)), sf_vars);path = cdr(path);#if MC_MODEL_DEBUGmc_model_trace_step_print(trace, step, TRACE_ITER_S_VARS, "S", i);
#endif}#if MC_MODEL_DEBUGStreamMgr_print_error(streams,  "nn");
#endifreturn trace;
}

node_ptr path
#if的具体作用是，如果满足条件语句，则编译器会把#if与#endif之间的代码编译进去。此处只编译，不执行。