Named-data network(NDN) introduces a data-centric manner for communication by assigning each data packet a corresponding name and letting application retrieve data by name, instead of by using communication tunnel between hosts. NDN architecture embed data authentication into network layer by requiring all data packets to be signed.
However, securing communication in network application is complicated even for experienced programmer. Design a secure system involves properly authentication of multiple entities and granting these entities with a minimal set of privileges.
NDN trust schema provide the ability to de-couple security logic from program logic. Using trust schema, programers could focus on design and implementation of bussiness logic, leaving network security part to NDN trust schema. Trust schema will match data packet’s name with security policy, then execute security checks, which usually are signature authentication.
To write a trust schema, a domain-specific language is purposed by [fn::https://named-data.net/wp-content/uploads/2015/06/ndn-0030-2-trust-schema.pdf]. The language utilize a regular-expression-like expression for expressing the data name matching, and a simple policy invocation rule to composite policies to form a hierarchical trust rule.
Defining a security policy is not a small matter.
One problem is that, since signature checking is an expensive operation, if a user defines a policy that might let a malicious user construct a circular signed data packets, computation resource might all be eaten by this authentication process, which will run forever. Therefore, we want to execute some property-checks on those policies, to make sure that, all check-passed policies, will terminate in a finite time, regardless of whatever data the policy is inspecting against.
System security follows the so-called ‘cask principle’: cask’s volume is decided on the shortest wood plate that consists the cask. A lot of security loopholes are origined in software’s specific implementation, instead of design. So, in this project, we apply program verification techniques on an implementation of this NDN trust schema interpreter, to formally proof that, as long as a policy can pass the termination check, it will terminate in a finite number of steps.
Firstly, to implemtent an interpreter, we implemented basic components of the policy language and type of data packets and network.
(*......*)
(*some basic type of language*)
Inductive Data : Type :=
| wrapped_data : Name -> Name -> Data -> Data
| data : Name -> Name -> Data.
Inductive MatchComp : Type :=
| mc_wild : MatchComp
| mc_sequence_wild : string -> MatchComp
| mc_exact : string -> MatchComp
| mc_indexed : MatchComp -> MatchComp.
Definition MatchPattern := list MatchComp.
(*......*)
(* program is a list of expressions*)
Inductive Expr : Type :=
| expr : RuleName -> MatchPattern -> Action -> Expr.
Inductive ExprLabeled : Type :=
| exprl : RuleName -> MatchPattern -> Action -> nat -> ExprLabeled.
Definition Program := list Expr.
(*......*)
The final design of checker is totally different from the original one. Checker can be viewed as two parts: a labeler and a label checker, similar to the techniques used in CompCert.
The labeler first label the program against the following specification:
- if there is prefix truncate in invoking parameter, n = 0
- if it is an anchor rule, n = 0
- otherwise, n = n’ + 1, where n’ is the called rule’s label
It label a expression in a program with a number indicating the upper bound of how many steps at most, the interpreter will take to have a reduction in arguments, or to terminate because of reaching trust anchor rule. This number will later be used only for reasoning about interpreter’s runtime behavior. In the concrete implementation, due to Coq’s limitation of function totality, there is a work around here. Since labeling need not take more than program length times to label all expression with final result, we simply set iterating times to be program length.
Fixpoint labelProgram (prog:Program) : ProgramLabeled :=
let n := List.length prog in
let progInitMiddle := (progInitLabel prog) in
let progFinalMidle := iterativeLabel n progInitMiddle in
progMiddle2Labled progFinalMidle.
Ideally, we need to proof this labeler will behave as label specification. But due to the time limitation, this part is missed right now. So, there might be a chance that a correct program is wrongly labeled, then it can not pass the label checker. But since label checker has been proofed, wrong program will not be accepted by label checker.
The second part, the label checker, is used to check that, if an expression has been labeled with number n, whether the expression has the corresponding behavior or not. So, only right program with right labels can pass this checker.
(* Must use function due to there are _ in matching,
coq can't unfold match with _*)
Function checkExpr (prog:ProgramLabeled) (e:ExprLabeled) : bool :=
let '(exprl _ _ act n2s) := e in
match act with
| actRc (ruleCall nxtRn nxtPl) =>
if Nat.eqb n2s 0
then (if hasPrefix nxtPl
then true
(*............................*)
To overcome the function totality restrain, the interpreter is implemented in a step-indexed way. For a given n, state will step n times, unless it gets a result in the middle.
Fixpoint interpr_step_main (n:nat) (st:State) : Rst :=
match n with
| 0 => unfinish
| S n' => let rst := interpr_step st in
match rst with
| state _ _ _ _ _ => interpr_step_main n' rst
| state_finished rtn => finished rtn
end
end.
From a top-to-down view, the proofs can be organized in the following way:
Firstly, the ultimate goal is to proof:
Forall prog
if (check program = true)
then (exists n rtn, interpreter n program = FINISHED rtn)
However, it is hard to directly proof this lemma. So, instead of proofing this lemma, we can also proof two similar lemmas that if combined those two, we can proof the ultimate goal in a classical logic easily.
Lemma interprMultiStepNSmaller :
forall st st' n,
checkState st = true ->
interpr_multi_step n st = st' ->
((exists rtn, st' = state_finished rtn)
\/
(forall prog' dt' net' e' args',
st' = (state prog' dt' net' e' args') ->
F st' <= F st - n)).
Lemma FzeroTerminate : forall st,
checkState st = true ->
F st = 0 -> (exists rtn, interpr_step st = state_finished rtn).
Here, the F function is a map from state to a natural number, which represents the maximum steps it need to terminate from this state. The number is caculated in this formula:
Fixpoint F (st:State) : nat :=
match st with
| (state prog dt net (exprl _ _ _ n) args) =>
(List.length prog) * (getNPrefix args) + n
| state_finished _ => 0
end.
Then, assume that forall n, interpr_multi_step n st does not terminate. let n = (F st), by interprMultiStepNSmaller, we know that F st’ = 0, and by FzeroTerminate, we know that st’ steps to a terminated state if F st’ = 0, then we have a contradiction. This proof need `excluded_middle` principle, which is not included in constructive logic.
To reason about the multi-step behavior, we need to proof some properties holds for single-step. The core lemma is to show that on each step, F st’ is strictly less than F st, unless it terminates.
Lemma step_result : forall st prog dt net e args st',
checkState st = true ->
(st = state prog dt net e args) ->
(interpr_step st = st') ->
(
(exists rtn, st' = state_finished rtn)
\/
(forall prog' dt' net' e' args', st' = (state prog' dt' net' e' args') -> F st' <= F st - 1)
).
Then, to proof this `step_result` lemma, we need to proof that those arguments, which are used to calculate F value, are getting smaller that resulting in deduction of F value. So the lemma here is:
Lemma step_args_smaller :
forall st prog dt net e a st' p' d' n' e' a' rn mp act n2s
rn' mp' act' n2s',
checkState st = true ->
st = state prog dt net e a ->
st' = state p' d' n' e' a' ->
e = exprl rn mp act n2s ->
e' = exprl rn' mp' act' n2s' ->
interpr_step st = st' ->
((n2s = 0 /\ (getNPrefix a' < getNPrefix a))
\/
(n2s' < n2s /\ (getNPrefix a' <= getNPrefix a))).
This is the longest proof in the whole project. Because we reason about state by its F value, to proof lemma, a common patter we used is to do a case analysis on all possible cases. Then we apply lemmas we gained from (checkState st = true) and lemmas of `interpr_step` function. After we get all we want, use omega to solve the equation automatically.
From a bottom-up view, to help proof the above goals, we extracted some lemmas from the implementation of interpr_step and checker.
For the `interpr_step`, we proofed that
- Program stay the same after step: Lemma progUntouchedAfterStep
- If there is prefix in the paramaters of calling, after genArgs, the prefix must shrink: Lemma `genArgs_lt_if_prefix`
- After genArgs, the prefix is less or equal to the previous: genArgs_le.
- Check-passed state implies that program and expression has passed the check: checkStateImply.
- If label n of state’s expression is zero, then it must has getPrefix bahaviour or it is an anchor: checkExprImply1.
- The label n of state’s expression is non-zero, it reflects its definition that the step count to next prefix shrink : Lemma checkExprImplyRc and checkExprImplyOr
- The label n of state meet the specification: Lemma labeled_prog_args_shrink_rc and labeled_prog_args_shrink_or
- Program’s length is longer than 0: Lemma progLengthLt0
- Each label n is less than program’s length: labelLtProgLength.
To summarize, except for Multi-Step-Smaller, which is apparently true if single-step-smaller holds, all important and major goals have been successfully proofed. To make it a theoretical perfect proof, all the admitted trivial lemmas should be proofed.
Compared with original goal, the difference is that the ‘try..else’ rule is removed in the project. ‘try…else’ and data encapsulating drastically make the proof more difficult, so it was removed at the time when I started to re-design the whole proof path. Proof of the concrete implementation is much harder than I expected. One reason is that, there are some Coq proof skills which take a lot of time to figure out, like, 1. avoiding unfold at beginning, because it will try to eagerly simplify the formula and ‘eat’ the term you want to keep, 2. use keyword Function instead of Fixpoint if there are ‘_’ or unused variable in matching, otherwise simpl or unfold will not work as expected in proof.
In the begining, the implementation used a recursive way like this:
Fixpoint f ....
match..
....some codes...
.... (f args...)
....some codes...
end
However, proofing in this recursive implementation is difficult. Recall that our goal is to proof that
forall prog, checked prog -> (exists n rtn, interpreter n prog env = Some rtn)
To proof this goal, one roadblock is that, for different data packets, you can not provide a specific rtn beforehand. Also, it is impossible to perform a case analysis on the return value, because the induction hypothesis needed has the form that, ‘down the way to the some point, there is a terminated state, and this state is no more than n steps further’, which seems like a customized induction hypothesis. However, the customized induction hypothesis might not be consistent with coq logic, and indeed it is not correct in this example.
It was the hardest part in the whole journey. But luckily, I came up an idea that I can map the state to a natural number, which indicates the maximum steps it will take to terminate from that state. Also, I found out that the formula F should can capture this. Then by labeling the expression and extract lemmas from label checker, finally, the goal is proofed.
The important experience I learn is the answers to questions like:
- what can be done
- what can be done easily
- what is hard or impossible to be done in coq
One ‘Aha moment’ during this journey is when I was trying to use dependent type to proof, I suddenly found one more reason why we need type system. Back to last quater’s 231, Professor Todd introduced Type-and-Effect systems. Todd gave an example of typing rules of a type system capturing exception catch and throw behaviours. At that time, one perplexing question for me is that, that system just looks too simple: bookkeeping exception behaviors in type. If we want to analyze the exception behavior, why can’t we just perform a code analysis on the concrete codes? Now I think I have a clear answer. Indeed, exception behavior analysis can be done both in type system level and code level. But the upshot is that, it is easier and more reasonable to be done in type system. Curry–Howard correspondence tells us that a type is a proposition and a program is a proof. Putting information into type is like to extend the proposition. Then all existing logical rules can be applied on this proposition, to help to form a sound theory. However, analysis on specific codes are just like reasoning about a proof of proposition. Even if it is possible, it is hard to reason that the algorithm used is correct.
An intuitive idea is that, the more powerful the type system is, the more information compiers or analyzers could use. On the other hand, the more powerful type system is, the more coding restrictions there are for a programmer. Type system is a linkage between program and logic. It enable compiers to rule out more errors, make IDE tools possible to perform precise codes refactoring, and code complement.
In daily programming works, nothing drives me to think about these questions. After design, implementation and unit-test, if everything is fine, codes are accepted. But in Coq, implementatin is the easy part, while proof is ten times harder. Back to the example of this project, putting information that only used in proof into types, like using dependent type, really makes proof easier, because more information can be extracted from the type.
Program verification techniques does improve software quality. During the proofing, I found several bugs in the implementation. That implementation, before proof started, has passed the unit-tests I set up. However, consider the countless hours spent on proofs, if I have spent the same amount of time on design or implementation, is it possible to rule out those bugs in the begining? Maybe yes, maybe no. Nonetheless, examples like CompCert showed that program verification techniques are useful in some cases. In my opinion, in the software engineering, the suitable scenario to use program verification techniques should have following characteristic: Firstly, It must be the key part of the whole system. Otherwise, it is not worthy to be proofed. Secondly, it must have a reasonable specification. Since there will always be a informal translate between software demand and specifications, if the demand is hard to be expressed in a formal specification, or the translation drastically fuzz up the demand, even if it is proofed, it is meaningless.
Also, even the essential complexity of verification in coq is in a same magnitude as it in software development, the accidental complexity of verification, at least in my experience, is much higher than it’s in software. To make coq a more popular tool, besides getting more people to understanding functional programming, coq need richer libraries, especially in proof automation. One example is a more powerful inversion. Sometime I met a situation like this:
H1 : match x with
| constructor1 .. => false
| constructor2 .. => false
| constructor3 .. => if a =? b then true else false
end = true
Apparently, only x is constructed by constructor3 and a = b. If I can get all these information by inversion on H1, a lot of time can be saved.
In the end of the day, I believe that program verification will become a critical part of software development process, combined with current techniques like unit-test, improving software quality. Yes, it’s just one of those things, but it definitely is the fanciest one.