Análise de código de sistemas de alta confiabilidade

Hello Habr! Neste artigo, quero falar sobre um tópico pouco discutido de análise de código para sistemas de alta confiabilidade. Existem muitos artigos sobre Habré sobre o que é uma boa análise estática, mas neste artigo eu gostaria de falar sobre o que é a verificação de código formal e também explicar os perigos do uso impensado de analisadores estáticos e padrões de codificação.



Havia muita controvérsia sobre como criar software com maior confiabilidade, metodologias, abordagens para a organização do desenvolvimento, ferramentas eram discutidas. Mas entre todas essas discussões, o que se perde é que o desenvolvimento de software é um processo , bastante bem estudado e formalizado. E se você olhar para esse processo, vai notar que ele se concentra não apenas em como o código é escrito / gerado, mas em como esse código é verificado. Mais importante ainda, o desenvolvimento requer o uso de ferramentas nas quais você pode "confiar".



Este breve tour acabou e vamos ver como o código é comprovadamente confiável. Primeiro, você precisa entender as características do código que atende aos requisitos de confiabilidade. O próprio termo "confiabilidade do código" parece um tanto vago e contraditório. Portanto, prefiro não inventar nada e, ao avaliar a confiabilidade do código, sou guiado pelos padrões da indústria, por exemplo, GOST R ISO 26262 ou KT-178C. O texto neles é diferente, mas a ideia é a mesma: o código confiável é desenvolvido de acordo com um único padrão (o chamado padrão de codificação ) e o número de erros de execução nele é minimizado. No entanto, nem tudo é tão simples aqui - os padrões prevêem situações em que, por exemplo, a conformidade com o padrão de codificação não é possível e tal desvio precisa ser documentado



Pântano perigoso MISRA e semelhantes



Os padrões de codificação têm como objetivo restringir o uso de construções de linguagem de programação que podem ser potencialmente perigosas. Em teoria, isso deve melhorar a qualidade do código, certo? Sim, isso garante a qualidade do código, mas é sempre importante lembrar que 100% de conformidade com as regras de codificação não é um fim em si mesmo. Se o código for 100% consistente com as regras de alguns MISRA, isso não significa de forma alguma que seja bom e correto. Você pode gastar muito tempo refatorando, limpando violações do padrão de codificação, mas tudo isso será perdido se o código acabar funcionando incorretamente ou contiver erros de tempo de execução. Além disso, as regras da MISRA ou CERT geralmente são apenas parte do padrão de codificação adotado na empresa.



A análise estática não é uma panacéia



Os padrões prescrevem uma revisão sistemática do código para encontrar defeitos no código e analisar o código para padrões de codificação.



As ferramentas de análise estática comumente usadas para esse propósito são boas para detectar falhas, mas não provam que o código-fonte está livre de erros de tempo de execução. E muitos erros detectados por analisadores estáticos são, na verdade, falsos positivos de ferramentas. Como resultado, o uso dessas ferramentas não reduz significativamente o tempo gasto na verificação do código devido à necessidade de verificar os resultados da verificação. Pior, eles podem não detectar erros de tempo de execução, o que é inaceitável para aplicativos que exigem alta confiabilidade.



Verificação formal de código



Portanto, os analisadores estáticos nem sempre são capazes de detectar erros de tempo de execução. Como eles podem ser detectados e eliminados? Nesse caso, é necessária a verificação formal do código-fonte.



Em primeiro lugar, você precisa entender que tipo de animal é? A verificação formal é a prova do código livre de erros usando métodos formais. Parece assustador, mas na verdade - é como uma prova de um teorema de Matan. Não há mágica aqui. Este método difere da análise estática tradicional, pois usa uma interpretação abstrataem vez de heurísticas. Isso nos dá o seguinte: podemos provar que não há erros específicos de tempo de execução no código. Quais são esses erros? Esses são todos os tipos de overruns de array, divisão por zero, estouro de inteiro e assim por diante. Sua maldade reside no fato de que o compilador irá coletar código contendo tais erros (uma vez que tal código está sintaticamente correto), mas quando este código for executado, eles aparecerão.



Vejamos um exemplo. Abaixo nos spoilers está o código para um controlador PI simples:



Ver código
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);







Vamos executar o teste com o Polyspace Bug Finder , um analisador estático certificado e qualificado, e obter os seguintes resultados:







Por conveniência, vamos tabular os resultados:



Ver resultados






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





E agora verificamos o mesmo código usando a ferramenta de verificação formal do Polyspace Code Prover:





Verde nos resultados é o código que comprovadamente não contém erros de tempo de execução. Vermelho - erro comprovado. Laranja - A ferramenta está sem dados. Os resultados marcados em verde são os mais interessantes. Se para uma parte do código a ausência de um erro de tempo de execução foi provada, então para esta parte do código a quantidade de teste pode ser reduzida significativamente (por exemplo, o teste de robustez não pode mais ser realizado). E agora, vamos olhar a tabela de resumo de erros potenciais e comprovados:



Ver resultados






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)







Esta tabela me diz o seguinte:



Houve um erro de tempo de execução na linha 93 que com certeza acontecerá. O restante dos avisos me diz que configurei a verificação incorretamente ou preciso escrever um código de segurança ou superá-los de outra maneira.



Pode parecer que a verificação formal é muito legal e todo o projeto deve ser verificado de forma incontrolável. No entanto, como acontece com qualquer instrumento, existem limitações, principalmente relacionadas aos custos de tempo. Em suma, a verificação formal é lenta. Tão lento. O desempenho é limitado pela complexidade matemática da própria interpretação abstrata e do volume do código a ser verificado. Portanto, você não deve tentar verificar rapidamente o kernel do Linux. Todos os projetos de verificação no Polyspace podem ser divididos em módulos que podem ser verificados independentemente uns dos outros, e cada módulo tem sua própria configuração. Ou seja, podemos ajustar a profundidade da verificação para cada módulo separadamente.





"Confie" nas ferramentas



Quando você lida com os padrões da indústria, como KT-178S ou GOST R ISO 26262, você constantemente se depara com coisas como "confiança em uma ferramenta" ou "qualificação de uma ferramenta". O que é isso? Este é um processo no qual você mostra que os resultados das ferramentas de desenvolvimento ou teste que foram usadas no projeto podem ser confiáveis ​​e seus erros são documentados. Esse processo é assunto para um artigo à parte, pois nem tudo é óbvio. O principal aqui é o seguinte: as ferramentas utilizadas na indústria sempre vêm com um conjunto de documentos e testes que auxiliam nesse processo.



Resultado



Com um exemplo simples, vimos a diferença entre a análise estática clássica e a verificação formal. Ele pode ser aplicado fora de projetos que exigem adesão aos padrões da indústria? Sim, é claro que você pode. Você pode até pedir uma versão de teste aqui .



A propósito, se você estiver interessado, pode fazer um artigo separado sobre certificação de instrumentos. Escreva nos comentários se precisar de tal artigo.



All Articles