高可靠性系统的代码分析

哈勃!在本文中,我想谈一谈关于高可靠性系统的代码分析的一个很少讨论的话题。在Habré上有很多文章介绍了什么是好的静态分析,但是在本文中,我想谈谈什么是正式的代码验证,并且还说明了不慎使用静态分析器和编码标准的危险。



关于如何创建具有更高可靠性的软件,方法论,开发组织方法和工具,存在很多争议。但是在所有这些讨论中,所丢失的是软件开发是一个过程,并且已经进行了充分的研究和形式化。并且,如果您看一下此过程,您会发现该过程不仅关注代码的编写/生成方式,而且关注于如何验证代码。最重要的是,开发需要使用您可以“信任”的工具。



这次简短的浏览已经结束,让我们看看如何证明代码是可靠的。首先,您需要了解满足可靠性要求的代码特征。术语“代码可靠性”看起来相当模糊和矛盾。因此,我不想发明任何东西,并且在评估代码的可靠性时,我会受到行业标准(例如GOST R ISO 26262或KT-178S)的指导。措辞不同,但是思想是相同的:可靠的代码是根据单一标准(所谓的编码标准)开发的,并且其中的运行时错误数量已降至最低。但是,这里的一切并不是那么简单-标准提供了以下情况:例如,无法遵守编码标准,并且需要记录这种偏差



危险的泥潭MISRA等



编码标准旨在限制可能具有潜在危险的编程语言构造的使用。从理论上讲,这应该提高代码的质量,对吗?是的,这可以确保代码的质量,但是记住100%遵守编码规则本身并不是目的,这一点始终很重要。如果某个代码100%符合某些MISRA的规则,那么这并不意味着它是正确和正确的。您可能需要花费大量时间进行重构,清理违反编码标准的行为,但是如果代码最终无法正常工作或包含运行时错误,所有这些都将被浪费掉。此外,MISRA或CERT的规则通常只是企业采用的编码标准的一部分。



静态分析不是万能药



这些标准规定了系统的代码审查,以便发现代码中的缺陷并分析代码以用于编码标准。



通常用于此目的的静态分析工具可以很好地发现缺陷,但是它们不能证明源代码没有运行时错误。静态分析仪检测到的许多错误实际上是工具的误报。结果,由于需要检查检查结果,因此使用这些工具不会大大减少检查代码所花费的时间。更糟糕的是,它们可能无法检测到运行时错误,这对于要求高可靠性的应用程序是不可接受的。



正式代码验证



因此,静态分析器并不总是能够捕获运行时错误。如何检测和消除它们?在这种情况下,需要对源代码进行正式验证。



首先,您需要了解它是哪种动物?形式验证是使用形式化方法对无错误代码的证明。听起来很吓人,但实际上-就像是Matan定理的证明。这里没有魔术。此方法与传统的静态分析不同,因为它使用抽象解释而不是试探法。这给了我们以下内容:我们可以证明代码中没有特定的运行时错误。这些错误是什么?这些都是各种数组溢出,被零除,整数溢出等。它们的意思在于,编译器将收集包含此类错误的代码(因为此类代码在语法上是正确的),但是在运行此代码时,它们将出现。



让我们来看一个例子。扰流器下面是一个简单的PI控制器的代码:



查看代码
pictrl.c
#include "pi_control.h"


/* Global variable definitions */
float inp_volt[2];
float integral_state;
float duty_cycle;
float direction;
float normalized_error;


/* Static functions */
static void pi_alg(float Kp, float Ki);
static void process_inputs(void);



/* control_task implements a PI controller algorithm that ../
  *
  * - reads inputs from hardware on actual and desired position
  * - determines error between actual and desired position
  * - obtains controller gains
  * - calculates direction and duty cycle of PWM output using PI control algorithm
  * - sets PWM output to hardware
  *
  */
void control_task(void)
{
  float Ki;
  float Kp;

  /* Read inputs from hardware */
  read_inputs();

  /* Convert ADC values to their respective voltages provided read failure did not occur, otherwise do not update input values */
  if (!read_failure)  {
    inp_volt[0] = 0.0048828125F * (float) inp_val[0];
    inp_volt[1] = 0.0048828125F * (float) inp_val[1];
  }  

  /* Determine error */
  process_inputs();
  
  /* Determine integral and proprortional controller gains */
  get_control_gains(&Kp,&Ki);
  
  /* PI control algorithm */
  pi_alg(Kp, Ki);

  /* Set output pins on hardware */
  set_outputs();
}



/* process_inputs  computes the error between the actual and desired position by
  * normalizing the input values using lookup tables and then taking the difference */
static void process_inputs(void)
{
  /* local variables */
  float rtb_AngleNormalization;
  float rtb_PositionNormalization;

  /* Normalize voltage values */
  look_up_even( &(rtb_AngleNormalization), inp_volt[1], angle_norm_map, angle_norm_vals); 
  look_up_even( &(rtb_PositionNormalization), inp_volt[0], pos_norm_map, pos_norm_vals);
	 
  /* Compute error */
  normalized_error = rtb_PositionNormalization - rtb_AngleNormalization;

}



/* look_up_even provides a lookup table algorithm that works for evenly spaced values.
  * 
  * Inputs to the function are...
  *     pY - pointer to the output value
  *     u - input value
  *     map - structure containing the static lookup table data...
  *         valueLo - minimum independent axis value
  *         uSpacing - increment size of evenly spaced independent axis
  *         iHi - number of increments available in pYData
  *         pYData - pointer to array of values that make up dependent axis of lookup table
   *
   */
void look_up_even( float *pY, float u, map_data map, float *pYData)
{
  /* If input is below range of lookup table, output is minimum value of lookup table (pYData) */
  if (u <= map.valueLo ) 
  {
    pY[1] = pYData[1];
  } 
  else 
  {
    /* Determine index of output into pYData based on input and uSpacing */
    float uAdjusted = u - map.valueLo;
    unsigned int iLeft = uAdjusted / map.uSpacing;
	
	/* If input is above range of lookup table, output is maximum value of lookup table (pYData) */
    if (iLeft >= map.iHi ) 
	{
      (*pY) = pYData[map.iHi];
    } 
	
	/* If input is in range of lookup table, output will interpolate between lookup values */
	else 
	{
      {
        float lambda;  // fractional part of difference between input and nearest lower table value

        {
          float num = uAdjusted - ( iLeft * map.uSpacing );
          lambda = num / map.uSpacing;
        }

        {
          float yLeftCast;  // table value that is just lower than input
          float yRghtCast;  // table value that is just higher than input
          yLeftCast = pYData[iLeft];
          yRghtCast = pYData[((iLeft)+1)];
          if (lambda != 0) {
            yLeftCast += lambda * ( yRghtCast - yLeftCast );
          }

          (*pY) = yLeftCast;
        }
      }
    }
  }
}


static void pi_alg(float Kp, float Ki)
{
  {
    float control_output;
	float abs_control_output;

    /*  y = integral_state + Kp*error   */
    control_output = Kp * normalized_error + integral_state;

	/* Determine direction of torque based on sign of control_output */
    if (control_output >= 0.0F) {
      direction = TRUE;
    } else {
      direction = FALSE;
    }

	/* Absolute value of control_output */
    if (control_output < 0.0F) {
      abs_control_output = -control_output;
    } else if (control_output > 0.0F) {
	  abs_control_output = control_output;
	}
	
    /* Saturate duty cycle to be less than 1 */
    if (abs_control_output > 1.0F) {
	  duty_cycle = 1.0F;
	} else {
	  duty_cycle = abs_control_output;
	}

    /* integral_state = integral_state + Ki*Ts*error */
    integral_state = Ki * normalized_error * 1.0e-002F + integral_state;
	  
  }
}






pi_control.h
/* Lookup table structure */
typedef struct {
  float valueLo;
  unsigned int iHi;
  float uSpacing;
} map_data;

/* Macro definitions */
#define TRUE 1
#define FALSE 0

/* Global variable declarations */
extern unsigned short inp_val[];
extern map_data angle_norm_map;
extern float angle_norm_vals[11];
extern map_data pos_norm_map;
extern float pos_norm_vals[11];
extern float inp_volt[2];
extern float integral_state;
extern float duty_cycle;
extern float direction;
extern float normalized_error;
extern unsigned char read_failure;

/* Function declarations */
void control_task(void);
void look_up_even( float *pY, float u, map_data map, float *pYData);
extern void read_inputs(void);
extern void set_outputs(void);
extern void get_control_gains(float* c_prop, float* c_int);







让我们使用经认证的合格静态分析器Polyspace Bug Finder运行测试,并获得以下结果:







为方便起见,我们将结果制成表格:



查看结果






Non-initialized variable

Local variable 'abs_control_output' may be read before being initialized.

159

Float division by zero

Divisor is 0.0.

99

Array access out of bounds

Attempt to access element out of the array bounds.

Valid index range starts at 0.

38

Array access out of bounds

Attempt to access element out of the array bounds.

Valid index range starts at 0.

39

Pointer access out of bounds

Attempt to dereference pointer outside of the pointed object at offset 1.

93





现在,我们使用Polyspace Code Prover正式验证工具来验证相同的代码:





结果中的绿色是已证明没有运行时错误的代码。红色-已证明错误。橙色-该工具没有数据。用绿色标记的结果是最有趣的。如果对于一部分代码已经证明没有运行时错误,那么对于这部分代码,可以大大减少测试量(例如,无法再进行健壮性测试)。现在,让我们看一下潜在和已证明错误的摘要表:



查看结果






Out of bounds array index

38

Warning: array index may be outside bounds: [array size undefined]

Out of bounds array index

39

Warning: array index may be outside bounds: [array size undefined]

Overflow

70

Warning: operation [-] on float may overflow (on MIN or MAX bounds of FLOAT32)

Illegally dereferenced pointer

93

Error: pointer is outside its bounds

Overflow

98

Warning: operation [-] on float may overflow (result strictly greater than MAX FLOAT32)

Division by zero

99

Warning: float division by zero may occur

Overflow

99

Warning: operation [conversion from float32 to unsigned int32] on scalar may overflow (on MIN or MAX bounds of UINT32)

Overflow

99

Warning: operation [/] on float may overflow (on MIN or MAX bounds of FLOAT32)

Illegally dereferenced pointer

104

Warning: pointer may be outside its bounds

Overflow

114

Warning: operation [-] on float may overflow (result strictly greater than MAX FLOAT32)

Overflow

114

Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

115

Warning: operation [/] on float may overflow (on MIN or MAX bounds of FLOAT32)

Illegally dereferenced pointer

121

Warning: pointer may be outside its bounds

Illegally dereferenced pointer

122

Warning: pointer may be outside its bounds

Overflow

124

Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

124

Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

124

Warning: operation [-] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

142

Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

142

Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)

Non-uninitialized local variable

159

Warning: local variable may be non-initialized (type: float 32)

Overflow

166

Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)

Overflow

166

Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)







该表告诉我以下内容:



肯定会发生第93行上的运行时错误。其余警告则告诉我,我是否正确配置了验证,或者我需要编写安全代码或以其他方式克服它们。



看起来,形式验证非常酷,应该对整个项目进行不可控制的验证。但是,与任何工具一样,存在一些限制,主要与时间成本有关。简而言之,正式验证很慢。太慢了。性能受到抽象解释本身和要验证的代码量的数学复杂性的限制。因此,您不应尝试快速验证Linux内核。Polyspace中的所有验证项目都可以分为可以相互独立验证的模块,并且每个模块都有自己的配置。也就是说,我们可以分别调整每个模块的验证完整性。





工具中的“信任”



当您处理诸如KT-178C或GOST R ISO 26262之类的行业标准时,就会不断遇到诸如“信任工具”或“工具资格”之类的问题。它是什么?在此过程中,您可以证明该项目中使用的开发或测试工具的结果可以信任,并且可以记录其错误。此过程是另一篇文章的主题,因为并非所有内容都是显而易见的。这里的主要内容是:行业中使用的工具总是附带一系列有助于此过程的文档和测试。



结果



通过一个简单的示例,我们研究了经典静态分析和形式验证之间的区别。可以将其应用到需要遵守行业标准的项目之外吗?是的,当然可以。您甚至可以在这里索取试用版



顺便说一句,如果您有兴趣,可以撰写有关仪器认证的单独文章。如果需要这样的文章,请在评论中写。



All Articles