Skip to content

Latest commit

 

History

History
536 lines (360 loc) · 20.4 KB

File metadata and controls

536 lines (360 loc) · 20.4 KB

十四、安全关键系统指南

嵌入式系统对代码质量的要求通常高于其他软件领域。由于许多嵌入式系统不需要监控昂贵的工业设备,因此出错的代价很高。在软件或硬件故障可能导致人员受伤甚至死亡的安全关键系统中,该风险甚至更高。此类系统的软件必须遵循特定的指导原则,旨在最大限度地减少调试和测试阶段未发现错误的机会。

在本章中,我们将通过以下方法探索安全关键系统的一些要求和最佳实践:

  • 使用所有函数的返回值
  • 使用静态代码分析器
  • 使用前置条件和后置条件
  • 探索代码正确性的形式验证

这些方法将帮助您理解安全关键系统的要求和指南,以及用于认证和一致性测试的工具和方法。

使用所有函数的返回值

C 或 C++ 语言都不要求开发人员使用任何函数返回的值。定义一个返回整数的函数,然后在代码中调用它,忽略它的返回值,这是完全可以接受的。

这种灵活性通常会导致难以诊断和修复的软件错误。最常见的情况是,函数返回错误代码。开发人员可能会忘记为经常使用且很少失败的函数添加错误条件检查,例如close

安全关键系统最广泛使用的编码标准之一是 MISRA。它定义了对 C 和 C++ 语言的要求——分别是 MISRA C 和 MISRA C++。最近推出的 Adaptive AUTOSAR 定义了汽车行业的编码指南。预计在不久的将来,自适应 AUTOSAR 指南将被用作更新后的 MISRA C++ 指南的基础。

针对 C++ 的 MISRA 和 AUTOSAR 编码指南(https://www . AUTOSAR . org/file admin/user _ upload/standards/adaptive/17-03/AUTOSAR _ RS _ CPP 14 guidelines . pdf)都要求开发人员使用所有非 void 函数和方法返回的值。相应的规则定义如下:

"Rule A0-1-2 (required, implementation, automated): The value returned by a function having a non-void return type that is not an overloaded operator shall be used."

在这个食谱中,我们将学习如何在我们的代码中使用这个规则。

怎么做...

我们将创建两个类,在一个文件中保存两个时间戳。一个时间戳指示实例创建的时间,而另一个时间戳指示实例销毁的时间。这对于代码分析非常有用,可以测量我们在一个函数或任何其他感兴趣的代码块中花费了多少时间。请遵循以下步骤:

  1. 在您的工作目录中,即~/test,创建一个名为returns的子目录。
  2. 使用您喜欢的文本编辑器在returns子目录中创建一个名为returns.cpp的文件。
  3. 将第一个类添加到returns.cpp文件中:
#include <system_error>

#include <unistd.h>
#include <sys/fcntl.h>
#include <time.h>

[[nodiscard]] ssize_t Write(int fd, const void* buffer,
                            ssize_t size) {
  return ::write(fd, buffer, size);
}

class TimeSaver1 {
  int fd;

public:
  TimeSaver1(const char* name) {
    int fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);
    if (fd < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to open file");
    }
    Update();
  }

  ~TimeSaver1() {
    Update();
    close(fd);
  }

private:
  void Update() {
    time_t tm;
    time(&tm);
    Write(fd, &tm, sizeof(tm));
  }
};
  1. 接下来,我们添加第二个类:
class TimeSaver2 {
  int fd;

public:
  TimeSaver2(const char* name) {
    fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);
    if (fd < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to open file");
    }
    Update();
  }

  ~TimeSaver2() {
    Update();
    if (close(fd) < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to close file");
    }
  }

private:
  void Update() {
    time_t tm = time(&tm);
    int rv = Write(fd, &tm, sizeof(tm));
    if (rv < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to write to file");
    }
  }
};
  1. main函数创建两个类的实例:
int main() {
  TimeSaver1 ts1("timestamp1.bin");
  TimeSaver2 ts2("timestamp2.bin");
  return 0;
}
  1. 最后,我们创建一个包含程序构建规则的CMakeLists.txt文件:
cmake_minimum_required(VERSION 3.5.1)
project(returns)
add_executable(returns returns.cpp)

set(CMAKE_SYSTEM_NAME Linux)
set(CMAKE_SYSTEM_PROCESSOR arm)

SET(CMAKE_CXX_FLAGS "--std=c++ 17")
set(CMAKE_CXX_COMPILER /usr/bin/arm-linux-gnueabi-g++)
  1. 现在,您可以构建和运行该应用。

它是如何工作的...

我们现在已经创建了两个类,TimeSaver1TimeSaver2,它们看起来几乎相同,做着相同的工作。两个类都在其构造函数中打开一个文件,并调用Update函数,该函数将时间戳写入打开的文件。

类似地,它们的析构函数调用相同的Update函数来添加第二个时间戳并关闭文件描述符。

然而TimeSaver1打破了 A0-1-2 规则,不安全。让我们仔细看看这个。其Update功能调用两个功能,timewrite。这两个函数都可能失败,返回正确的错误代码,但是我们的实现忽略了它:

    time(&tm);
    Write(fd, &tm, sizeof(tm));

此外,TimeSaver1的析构函数通过调用close函数关闭打开的文件。这也可能失败,返回一个我们忽略的错误代码:

    close(fd);

第二类TimeSaver2符合要求。我们将时间调用的结果分配给tm变量:

    time_t tm = time(&tm);

如果Write返回错误,我们抛出异常:

    int rv = Write(fd, &tm, sizeof(tm));
    if (rv < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to write to file");
    }

同样,如果close返回错误,我们抛出异常:

    if (close(fd) < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to close file");
    }

为了缓解这种问题,C++ 17 标准引入了一个名为[[nodiscard]]的特殊属性。如果一个函数用这个属性声明,或者它返回一个标记为nodiscard的类或枚举,如果它的返回值被丢弃,编译器应该显示一个警告。为了使用这个特性,我们在write函数周围创建了一个自定义包装器,并将其声明为nodiscard:

[[nodiscard]] ssize_t Write(int fd, const void* buffer,
                            ssize_t size) {
  return ::write(fd, buffer, size);
}

当我们构建应用时,我们可以在编译器输出中看到这一点,这也意味着我们有机会修复它:

事实上,编译器能够识别并报告我们代码中的另一个问题,我们将在下一个配方中讨论。

如果我们构建并运行该应用,我们将看不到任何输出,因为所有的写入都指向文件。我们可以运行ls命令来检查程序是否产生结果,如下所示:

$ ls timestamp*

由此,我们得到以下输出:

不出所料,我们的程序创建了两个文件。它们应该是相同的,但它们不是。TimeSaver1创建的文件为空,说明其实现有问题。

TimeSaver2生成的文件是有效的,但这是否意味着其实现是 100%正确的?不一定,我们将在下一个食谱中看到。

还有更多...

更多关于[[nodiscard]]属性的信息可以在它的参考页面上找到。从 C++ 20 开始,nodiscard属性可以包含一个字符串文字,解释为什么值不应该被丢弃;例如[[nodiscard("Check for write errors")]]

重要的是要理解,遵守安全准则确实会使您的代码更安全,但并不能保证它。在TimeSaver2的实现中,我们使用time返回的值,但是不检查它是否有效。相反,我们无条件地写入输出文件。同样,如果write返回一个非零数字,它仍然可以向文件中写入比请求更少的数据。即使您的代码在形式上符合准则,它也可能包含相关的问题。

使用静态代码分析器

所有安全指南都被定义为对源代码或应用设计的大量特定要求。这些需求中的许多可以通过使用静态代码分析器来自动检查。

静态代码分析器是可以分析源代码的工具,如果开发者检测到违反代码质量要求的代码模式,就会发出警告。在错误检测和预防方面,它们效率极高。因为它们可以在代码构建之前运行,所以在开发的最早阶段就修复了许多错误,而不涉及耗时的测试和调试过程。

除了错误检测和预防,静态代码分析器还用于在认证过程中证明代码符合目标要求和指南。

在本食谱中,我们将学习如何在应用中使用静态代码分析器。

怎么做...

我们将创建一个简单的程序,并运行众多开源代码分析器中的一个来检查潜在的问题。请遵循以下步骤:

  1. 转到~/test/returns目录,这是我们在之前的食谱中创建的。
  2. 从存储库中安装cppcheck工具。确保你在root账户下,而不是user账户下:
# apt-get install cppcheck
  1. 再次转到user账户:
# su - user
$
  1. returns.cpp文件运行cppcheck:
$ cppcheck --std=posix --enable=warning returns.cpp
  1. 分析它的输出。

它是如何工作的...

代码分析器可以解析我们应用的源代码,并根据大量代表不良编码实践的模式对其进行测试。

存在许多代码分析器,从开源和免费使用到企业使用的昂贵商业产品。

中提到的 MISRA 编码标准使用所有功能的返回值配方是一个商业标准。这意味着您需要购买许可证才能使用它,同样,也需要购买经过认证的代码分析器来测试代码是否符合 MISRA。

出于学习目的,我们将使用名为cppcheck的开源代码分析器。它被广泛使用,并且已经包含在 Ubuntu 存储库中。我们可以用与任何其他 Ubuntu 包相同的方式安装它:

# apt-get install cppcheck $ cppcheck --std=posix --enable=warning returns.cpp

现在,我们将源文件名作为参数传递。检查速度很快,会生成以下报告:

正如我们所看到的,它在我们的代码中检测到了两个问题,甚至在我们试图构建它之前。第一期在我们更安全,增强的TimeSaver2班!为了使其符合 A0-1-2 的要求,我们需要检查close返回的状态码,如果出现错误就抛出异常。然而,我们在析构函数中这样做,破坏了 C++ 错误处理机制。

代码分析器检测到的第二个问题是资源泄漏。这就解释了为什么TimeSaver1会生成空文件。打开文件时,我们不小心将文件描述符分配给了局部变量,而不是实例变量,即fd:

int fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);

现在,我们可以修复它们并重新运行cppcheck以确保问题已经过去,并且没有引入新的问题。使用代码分析器作为开发工作流的一部分可以使您的代码更安全,性能更快,因为您可以在开发周期的早期阶段检测和预防问题。

还有更多...

虽然cppcheck是一个开源工具,但是它支持大量的 MISRA 检查。这并不能使它成为验证符合 MISRA 指南的认证工具,但可以让您了解您的代码离 MISRA 要求有多近,以及需要付出多少努力才能使其符合。

MISRA 检查是作为附加组件实现的;您可以根据cppcheck(https://github.com/danmar/cppcheck/tree/master/addons)的 GitHub 存储库的加载项部分中的说明运行它。

使用前置条件和后置条件

在前面的食谱中,我们学习了如何在开发的早期阶段使用静态代码分析器来防止编码错误。另一个强大的防错工具是契约编程

契约式编程是一种实践,在这种实践中,开发人员为函数或模块的输入值、结果和中间状态明确定义契约或期望。虽然中间状态取决于实现,但是输入和输出值的契约可以被定义为公共接口的一部分。这些期望分别被称为前提条件前提条件,有助于避免定义模糊的接口导致的编程错误。

在这个食谱中,我们将学习如何在我们的 C++ 代码中定义前置条件和后置条件。

怎么做...

为了测试前置条件和后置条件是如何工作的,我们将部分重用我们在前面的食谱中使用的 TimeSaver1 类的代码。请遵循以下步骤:

  1. 在您的工作目录中,即~/test,创建一个名为assert的子目录。
  2. 使用您喜欢的文本编辑器在assert子目录中创建一个名为assert.cpp的文件。
  3. TimeSaver1类的修改版本添加到assert.cpp文件中:
#include <cassert>
#include <system_error>

#include <unistd.h>
#include <sys/fcntl.h>
#include <time.h>

class TimeSaver1 {
  int fd = -1;

public:
  TimeSaver1(const char* name) {
    assert(name != nullptr);
    assert(name[0] != '\0');

    int fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);
    if (fd < 0) {
      throw std::system_error(errno,
                              std::system_category(),
                              "Failed to open file");
    }
    assert(this->fd >= 0);
  }

  ~TimeSaver1() {
    assert(this->fd >= 0);
    close(fd);
  }
};
  1. 接下来是一个简单的main函数:
int main() {
  TimeSaver1 ts1("");
  return 0;
}
  1. 将构建规则放入CMakeLists.txt文件:
cmake_minimum_required(VERSION 3.5.1)
project(assert)
add_executable(assert assert.cpp)

set(CMAKE_SYSTEM_NAME Linux)
set(CMAKE_SYSTEM_PROCESSOR arm)

SET(CMAKE_CXX_FLAGS "--std=c++ 11")
set(CMAKE_CXX_COMPILER /usr/bin/arm-linux-gnueabi-g++)
  1. 现在,您可以构建和运行该应用。

它是如何工作的...

在这里,我们重用了上一个食谱中TimeSaver1类的一些代码。为了简单起见,我们去掉了Update方法,只留下了它的构造函数和析构函数。

我们有意保留静态代码分析器在前面的配方中发现的相同错误,以检查前置条件和后置条件检查是否可以用于防止此类问题。

我们的构造函数接受文件名作为参数。我们对文件名没有任何特别的限制,除了它应该是有效的。两个明显无效的文件名如下:

  • 作为名称的空指针
  • 空名字

我们使用assert宏将这些规则作为先决条件:

assert(name != nullptr);
assert(name[0] != '\0');

要使用这个宏,我们需要包含一个头文件,即csassert:

#include <cassert>

接下来,我们使用文件名打开文件,并将其存储在fd变量中。我们将其分配给局部变量,即fd,而不是实例变量fd。这是我们想要检测的编码错误:

int fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);

最后,我们在构造函数中加入后置条件。在我们的例子中,唯一的后置条件是实例变量fd应该有效:

assert(this->fd >= 0);

请注意,我们如何在它前面加上这个前缀,以消除它与局部变量的歧义。同样,我们给析构函数添加一个前提条件:

assert(this->fd >= 0);

我们在这里不添加任何后置条件,因为在析构函数返回后,实例不再有效。

现在,让我们测试我们的代码。在main函数中,我们创建一个TimeSaver1的实例,传递一个空文件名作为参数:

TimeSaver1 ts1("");

构建并运行程序后,我们将看到以下输出:

构造函数中的前提条件检查检测到违反合同并终止了应用。让我们将文件名更改为有效的文件名:

TimeSaver1 ts1("timestamp.bin");

我们再次构建并运行应用,得到不同的输出:

现在,所有先决条件都已满足,但是我们违反了后置条件,因为我们未能更新实例变量fd。通过删除fd前的类型定义来更改第 16 行,如下所示:

fd = open(name, O_RDWR|O_CREAT|O_TRUNC, 0600);

重新构建并再次运行程序会产生一个空输出:

这表明对输入参数和结果的所有期望都已满足。即使是最基本的形式,使用契约进行编程也能帮助我们避免两个编码问题。这就是为什么这项技术被广泛应用于软件开发的所有领域,尤其是安全关键系统。

还有更多...

C++ 20 标准中有望增加对契约式编程更详细的支持。然而,它被推迟到以后的标准。提案说明见 g .多斯·雷斯、J. D .加西亚、j .拉科斯、A .梅雷迪思、n .迈尔斯、b .斯特劳德普的论文A Contract Design(http://www . open-STD . org/JT C1/sc22/wg21/docs/papers/2016/p 0380 r 1 . pdf)。

探索代码正确性的形式验证

静态代码分析器和契约式编程方法帮助开发人员显著减少代码中的编码错误。然而,这在安全关键的软件开发中是不够的。正式证明软件组件的设计是正确的很重要。

有许多相当复杂的方法可以做到这一点,还有自动化这个过程的工具。在这个食谱中,我们将探索一种正式的软件验证工具,叫做 CPAchecker(https://cpachecker.sosy-lab.org/index.php)。

怎么做...

我们将下载并安装CPAcheck到我们的构建环境中,然后针对一个示例程序运行它。请遵循以下步骤:

  1. 打开包含您的构建环境的终端。
  2. 请确保您拥有根权限。如果没有,按下 Ctrl + D 退出用户会话返回会话。
  3. 安装 Java 运行时:
# apt-get install openjdk-11-jre
  1. 切换到用户会话,将目录改为/mnt:
# su - user
$ cd /mnt
  1. 下载并解压CPACheck档案,如下所示:
$ wget -O - https://cpachecker.sosy-lab.org/CPAchecker-1.9-unix.tar.bz2 | tar xjf -
  1. 将目录更改为CPAchecker-1.9-unix:
$ cd CPAchecker-1.9-unix
  1. 对示例文件运行CPAcheck:
./scripts/cpa.sh -default doc/examples/example.c 
  1. 下载故意包含错误的示例文件:
$ wget https://raw.githubusercontent.com/sosy-lab/cpachecker/trunk/doc/examples/example_bug.c
  1. 对新示例运行检查器:
./scripts/cpa.sh -default example_bug.c 
  1. 切换到网络浏览器,打开工具生成的~/test/CPAchecker-1.9-unix/output/Report.html报告文件。

它是如何工作的...

要运行CPAcheck,我们需要安装 Java 运行时。这在 Ubuntu 资源库中有,我们用apt-get来安装。

下一步是下载CPAcheck本身。我们使用wget工具下载归档文件,并立即将其输入到tar实用程序进行提取。完成后,可以在CPAchecker-1.9-unix目录中找到该工具。

我们使用一个预打包的示例文件来检查该工具的工作方式:

./scripts/cpa.sh -default doc/examples/example.c

它生成以下输出:

我们可以看到,该工具没有发现该文件的任何问题。CPAcheck档案中没有包含 bug 的类似文件,但我们可以从其网站下载:

$ wget https://raw.githubusercontent.com/sosy-lab/cpachecker/trunk/doc/examples/example_bug.c

我们再次运行该工具,并获得以下输出:

现在,结果不同了:检测到一个错误。我们可以打开工具生成的 HTML 报告进行进一步分析。除了日志和统计数据之外,它还显示了流程自动化图:

形式验证方法和工具很复杂,可以处理相对简单的应用,但它们保证了所有情况下应用逻辑的正确性。

还有更多...

你可以在 CPAchecker 的网站(https://cpachecker.sosy-lab.org/index.php)上找到更多关于它的信息。