Verification of complex software code using a modularized architecture
A technique verifies a compound software code using a modularized architecture. The compound software code may be divided into smaller components or modules that provide various functions (e.g., services) of the code. A set of properties may be defined for the modules, such that the verification technique may be used to verify that the modules manifest those properties, wherein at least one property may be security related and the remaining properties may be related to the services of the modules. The compound software code is divided into smaller modules to facilitate verification of the properties related to the services provided by the modules. Properties of the modules may be verified in accordance with an enhanced verification procedure to demonstrate that the modules manifest those properties and transform those modules into verified code bases (VCBs). The services of the VCBs may then be combined to provide functionality of the compound software code using well-defined interfaces, such as application programming interfaces (APIs).
1. A method comprising:
storing a compound software code in a memory connect to a central processing unit (CPU) adapted to execute the compound software code, the compound software code being divided into modules;
verifying that the compound software code implements a first property by verifying one or more second properties of the modules using an enhanced verification procedure to demonstrate that the modules manifest the one or more second properties and to transform the modules into verified code bases (VCBs), each VCB having an operational model, the enhanced verification procedure including (i) generating an executable of the operational model of a corresponding VCB, (ii) capturing a state dump of the executable of the operational model, (iii) capturing a corresponding state dump of an executable of the corresponding VCB, and (iv) iteratively comparing states of the executable of the operational model and the executable of the corresponding VCB until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that a respective second property is implemented by the corresponding VCB; and
executing services of the VCBs on the CPU in combination to provide functionality of the compound software code using interfaces.
2. The method of claim 1 wherein verifying the one or more second properties comprises:
executing the operational model in a functional programming language.
3. The method of claim 1 wherein the one or more second properties of the modules are subordinate properties that include at least one security related property and one or more service related second properties of the VCBs.
4. The method of claim 1 wherein the interfaces are application programming interfaces (APIs) and wherein verifying the one or more second properties of the modules includes verifying the APIs of the VCBs.
5. The method of claim 4 wherein executing the combined services of the VCBs comprises:
communicating with one of a trusted code base (TCB) and other VCBs using the verified APIs and an additional API of the TCB, wherein the VCBs are disposed over the TCB.
6. The method of claim 1 wherein each VCB has size of lines of software code that enables verification of the respective second property using the enhanced verification procedure.
7. The method of claim 5 wherein
the VCBs are organized as one or more groups according to the verified properties and wherein one or more of the verified APIs of each group of VCBs are exposed to invoke services of a respective group of VCBs.
8. The method of claim 7 wherein a verified set of second properties of a first group is different from the verified set of second properties of a second group.
9. A system comprising:
a central processing unit (CPU) configured to execute a compound software code divided into modules; and
a memory configured to store the modules, the compound software code verified to implement a first property by an enhanced verification to demonstrate that the modules manifest one or more second properties to transform the modules into verified code bases (VCBs), each VCB having an operational model, the services of the VCBs combined to provide functionality of the compound software code using interfaces, the enhanced verification configured to:
generate an executable of the operational model of a corresponding VCB;
capture a state dump of the executable of the operational model;
capture a corresponding state dump of an executable of the corresponding VCB; and
iteratively compare states of the executable of the operational model and the executable of the corresponding VCB until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that a respective second property is implemented by the corresponding VCB.
10. The system of claim 9 wherein the executable of the operational model is executed in a functional programming language.
11. The system of claim 9 wherein the one or more second properties are subordinate properties that include at least one security related property and one or more service related second properties of the VCBs.
12. The system of claim 9 wherein the interfaces are application programming interfaces (APIs) and wherein the enhanced verification further verifies the APIs of the VCBs.
13. The system of claim 12 wherein the VCBs are disposed over a trusted code base (TCB) in a configuration that enables communication with one of the TCB and the VCBs using the verified APIs and an additional API of the TCB.
14. The system of claim 13 wherein each VCB has a size of lines of software code that enables the enhanced verification of the respective second property.
15. The system of claim 14 wherein the VCBs are organized as one or more groups according to verified second properties.
16. The system of claim 13 wherein the verified APIs implement one or more third properties subordinate to the one or more second properties.
17. The system of claim 15 wherein the verified second properties of a first group are different from the verified second properties of a second group.
18. A non-transitory computer readable medium including program instructions for execution on a processor of a node on a network, the program instructions divided into modules configured to:
execute services using interfaces, wherein the program instructions are verified to implement a first property by verifying second properties of the modules using an enhanced verification procedure to demonstrate that the modules manifest the properties to transform the modules into verified code bases (VCBs), each VCB having an operational model, the enhanced verification procedure including (i) generating an executable of the operational model of a corresponding VCB, (ii) capturing a state dump of the executable operational model, (iii) capturing a corresponding state dump of an executable of the corresponding VCB, and (iv) iteratively comparing states of the executable of the operational model and the executable of the corresponding VCB until a predetermined number of the states match, wherein the predetermined number of matched states correspond to a predetermined level of confidence that the second property is implemented by the corresponding VCB; and
combine the services of the VCBs to provide functionality of the program instructions using the interfaces.
19. The non-transitory computer readable medium of claim 18 wherein the respective executable of the operational model is executed in a functional programming language.
20. The non-transitory computer readable medium of claim 18 wherein the interfaces are application programming interfaces (APIs) and wherein the enhanced verification procedure further verifies the APIs of the VCBs.