证明“无腐败”在Haskell [英] Proving "no corruption" in Haskell

问题描述

我在一个安全关键行业工作，我们的软件项目一般都有安全要求;我们必须证明软件的确实性很高。通常这些都是消极的，例如不应该比1更频繁地腐化。 （我应该补充说这些要求来自统计系统安全要求）。

腐败的一个来源显然是编码错误，我想用Haskell类型系统来至少排除某些类别的这些错误。像这样的东西：

首先，这里是我们的关键数据项目，不能损坏。

  newtype Critical = Critical String 
  

现在我想将这个项目存储在一些其他结构。

  data Foo = Foo整数关键
数据Bar = Bar String Critical 
  

现在我想写一个从Foo到Bar的转换函数，它保证不会与关键数据混淆。

  goodConvert，badConvert :: Foo  - > Bar 
 
 goodConvert（Foo nc）= Bar（显示n）c 
 
 badConvert（Foo n（Critical s））= Bar（显示n）（Critical $Bzzt  - ++ s）
  

我想要goodConvert来检查类型，但是badConvert要失败检查。

显然，我可以小心不要将Critical构造函数导入到进行转换的模块中。但是如果我可以在类型中表达这个属性会更好，因为那样我就可以构建保证保留这个属性的函数。

我试过了在不同的地方添加幻像类型和forall，但这没有帮助。

有一件事情可行的是不导出Critical构造函数，然后

  mkCritical :: String  - > IO关键
  

由于这些关键数据项创建的唯一位置是在输入函数中，因此这使得有些意义。但我更喜欢更优雅和通用的解决方案。

编辑

在评论中，FUZxxl建议看看 Safe Haskell 。这看起来像是最好的解决方案。不像我最初想要的那样在类型级别添加无损修饰符，它看起来像你可以在模块级别完成，如下所示：

1：创建一个导出Critical数据类型的所有功能（包括其构造函数）的Critical模块。在标题中加入{ - ＃LANGUAGE Unsafe＃ - }标记为不安全。

除了构造函数和可能用于破坏临界值的任何其他函数之外的所有内容。将此模块标记为值得信赖。

3：将处理临界值所需的任何模块标记为安全。然后使用这个来证明任何导入为安全的函数都不会导致损坏到Critical值。

这会留下少量的代码，例如输入代码解析关键值，需要进一步验证。我们无法消除这个代码，但减少需要详细验证的数量仍然是一个重要的胜利。

该方法基于这样的事实：函数不能创建新的值，除非函数返回它。如果一个函数只获得一个Critical值（如上面的convert函数），那么它是唯一可以返回的值。

当一个函数有两个或更多相同类型的临界值时;它必须保证不混淆。例如，

  swapFooBar ::（Foo，Bar） - > （Bar，Foo）
 swapFooBar（Foo n c1，Bar s c2）=（Bar s c1，Foo n c2）
  

然而，这可以通过对包含数据结构给予相同的处理来处理。 可以使用参数来获得中间值b / b
$ b

 数据Foo c = Foo整数c 
数据Bar c = Bar字符串c 
 
 goodConvert :: Foo c  - > Bar c 
 goodConvert（Foo nc）= Bar（show n）c 
  

由于 c 是一个不受约束的类型变量，您知道函数 goodConvert 无法知道任何关于 c ，因此不能构造该类型的不同值。它必须使用输入中提供的那个。

好吧，差不多。底部值可以让您打破这种保证。但是，您至少知道如果您尝试使用损坏的值，则会导致异常（或未终止）。

  badConvert :: Foo c  - > Bar c 
 badConvert（Foo n c）= Bar（show n）undefined 
  

I work in a safety-critical industry, and our software projects generally have safety requirements imposed; things that we have to demonstrate that the software does to a high degree of certainty. Often these are negatives, such as " shall not corrupt more frequently than 1 in ". (I should add that these requirements come from statistical system safety requirements).

One source of corruption is clearly coding errors, and I would like to use the Haskell type system to exclude at least some classes of these errors. Something like this:

First, here is our critical data item that must not be corrupted.

newtype Critical = Critical String

Now I want to store this item in some other structures.

data Foo = Foo Integer Critical
data Bar = Bar String Critical

Now I want to write a conversion function from Foo to Bar which is guaranteed not to mess with the Critical data.

goodConvert, badConvert :: Foo -> Bar

goodConvert (Foo n c) = Bar (show n) c

badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)

I want "goodConvert" to type check, but "badConvert" to fail type checking.

Obviously I can carefully not import the Critical constructor into the module that does conversion. But it would be much better if I could express this property in the type, because then I can compose up functions that are guaranteed to preserve this property.

I've tried adding phantom types and "forall" in various places, but that doesn't help.

One thing that would work would be to not export the Critical constructor, and then have

mkCritical :: String -> IO Critical

Since the only place that these Critical data items get created is in the input functions, this makes some sense. But I'd prefer a more elegant and general solution.

Edit

In the comments FUZxxl suggested a look at Safe Haskell. This looks like the best solution. Rather than adding a "no corruption" modifier at the type level as I originally wanted, it looks like you can do it at the module level, like this:

1: Create a module "Critical" that exports all the features of the Critical data type, including its constructor. Mark this module as "unsafe" by putting "{-# LANGUAGE Unsafe #-}" in the header.

2: Create a module "SafeCritical" that re-exports everything except the constructor and any other functions that might be used to corrupt a critical value. Mark this module as "trustworthy".

3: Mark any modules that are required to handle Critical values without corruption as "safe". Then use this to demonstrate that any function imported as "safe" cannot cause corruption to a Critical value.

This will leave a smaller minority of code, such as input code that parses Critical values, requiring further verification. We can't eliminate this code, but reducing the amount that needs detailed verification is still a significant win.

The method is based on the fact that a function cannot invent a new value unless a function returns it. If a function only gets one Critical value (as in the "convert" function above) then that is the only one it can return.

A harder variation of the problem comes when a function has two or more Critical values of the same type; it has to guarantee not to mix them up. For instance,

swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)

However this can be handled by giving the same treatment to the containing data structures.

解决方案

You can use parametricity to get partway there

data Foo c = Foo Integer c
data Bar c = Bar String c

goodConvert :: Foo c -> Bar c
goodConvert (Foo n c) = Bar (show n) c

Since c is an unconstrained type variable, you know that the function goodConvert cannot know anything about c, and therefore cannot construct a different value of that type. It has to use the one provided in the input.

Well, almost. Bottom values allow you to break this guarantee. However, you at least know that if you try to use a "corrupted" value, it will result in an exception (or non-termination).

badConvert :: Foo c -> Bar c
badConvert (Foo n c) = Bar (show n) undefined

这篇关于证明“无腐败”在Haskell的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！