Home

complete thesis as PDF

1. eee 20 Example of Isar proofs in Isabelle seen 20 yum command to install XEMACS 000 ee esse ceseceeeeeeeeecaeceseesseeeeaeecaeenseeees 20 Installation Instruction of Isabelle 2008 From Ref 16 21 xcb xlib error while installing Specware version 4 2 2 in Fedora 8 21 Modetng Approaches dios tasth RDUM dba les astutia nad M qe aon 26 Type Color definition in Spec ware uio ete acea docpaec tte bs etma gae pau i ee euda 27 Type Color definition in Isabelle eene 27 Light changes definition in Specware essen 27 Light changes definition in Isabelle 5a Dexter eiit 27 Specware specification representing the transition from color to color in list and a trivial theorem eseeeeeseseesessseeseesseserssresstssrssresseseresressessresresseeseesees 28 Translated Isabelle specification for transition from color to color in list and THe trivial theorems oiea ae Aee corte Ae tact aE ERS 29 Screenshot of Isabelle command menu eee 30 A counter example is found by Isabelle before using the two axioms 30 After the two axioms are applied Isabelle only need to prove one subgoal 31 Isabelle proof for theorem light matches for traffic light represented using list of COlOr fe 3l Traffic light modeled as a tuple of color and the number of state changes 32 Translated Isabelle specific
2. This theorem is trying to verify that for all traffic light light change equal to next state theorem light matches is fa x Traffic Light light_changes project 1 x project 1 next_state x Figure 5 Theorem Definition in Traffic Light Model 13 e Set and List In higher order logic it is customary to define a set as a predicate which is true exactly for i e for all and only the elements of the set Support for the Set specification is new in Specware version 4 2 5 and documentation on Set is not yet available in the Specware Language Manual at the time of this writing Unlike List which comes with a number of helper operations to search and manipulate members of the List Set is essentially a predicate which does not allow enumeration of each of its members From the comment inside the Set specification it is important to note that Sets as defined are useful only for specification purposes and not for execution f Monads The concept of Monads arises from category theory about which this thesis will not go into detail A Monad is a kind of abstract data type used to represent computations instead of data in the domain model in a functional programming language where a program is written as a set of equations where the value of an expression depends only on its free variables and not the order of computation In this context Monads allows the performance of impure sequential operations i
3. 2008 As this library is new we analyzed the Set specification itself to learn about the inbuilt operations and their uses Unlike the List Base Library which comes with a set of 80 utility functions for transversal and manipulation the Set Library does not provide many support functions For example the Member function is the only retrieval operation available and it works on a Singleton set i e a set containing only a single element A conscious effort had been made in the model to use sets as much as possible as it is most natural and appropriate for the LPSK model where sets of resources and associated properties are considered The team recognizes that some of the expressions in our model appear overly cumbersome and suspect that there may be better and more concise ways to represent them The refinement of the specification has been left as a potential scope of later work when proper documentation and practical examples of the Specware Set Base Library are made available Readers should note that the team has chosen to go down the track of just modeling flows related to exported resources Flow effects have been specified only in terms of the flows between subjects RsSet and exported resources ReSet For example flow has been declared as a tuple of subject exported resource and a set of flow mode For the model to be more complete e g with respect to noninterfernace additional axioms and properties may have to be defi
4. b4objMem lt get resource memory at obj write op at subj at obj afterobjMem lt get resource memory at obj return x memsect Set Bit memsect lt b4objMem amp amp memsect lt at subj rscmem amp amp memsect lt afterobjMem else return false op evalProgram InputList System StateMonad List Boolean def evalProgram inputs sys case inputs of gt return inp r inputs gt rl transition inp sys res evalProgram r inputs sys return rl res ECKE EK AIR BRK OE OCT KK KORE OK EU E DN KORR OK OR Ke UC OD TERK DEOR IKK OK OK Ee X OE OK DK KOK Kc o e e e eee Partial Ordering of BB Semantics to describe flows between blocks to be defined in such a way that information is not allowed to flow circularly i e if information leaves a block there is no transitive flow that will lead back to itself Important to note that any 2 blocks are not required to be related by a flow FOR FEDORA IPR AIRE BIER FIRE EEK TK GRIS Ke IG GUN CORO DOR RRR KO GN DIGOR ERR KE KEE CORR oe Ke eU ERIC op direct flow to bb BBMatrix a BlockId b BlockId Boolean Write in BB bb a b 5 a gt b caused by a Read in BB bb b a a gt b caused by b op PO blkset BSet bb BBMatrix Boolean fa i Block j Block k Block i in blkset amp amp j in blkset amp amp k in blkset gt oe Refective Property direct flow
5. x y 00 Figure 98 State Transformers for accessing and changing the State 2 This example is reproduced from an internet tutorial 19 with some changes in wording 91 gcdST StateTrans ImpState Int gcdST do x lt getX y lt getY if x y then return x else if x y then do putY y x gcdST else do putX x y gcdST Figure 99 Haskell Specification And finally a function to construct an initial state run the program and discard the final state as shown in Figure 100 greatestCommonDivisor x y snd applyST gcdST x y Figure 100 Encapsulating GCD function This small example only hints at the utility of Monads It would be much shorter to write the algorithm in a conventional functional style For one thing Monads provide access to global state and the savings from not having to explicitly pass the state around become larger as the program itself becomes larger B CORRESPONDING EXAMPLE IN SPECWARE We create a Specware model corresponding to the Haskell one to calculate GCD 92 5 Contains the current values of the 2 inputs to calculate gcd on type GCDState Nat Nat Figure 101 Declaration of GCDState A StateMonad is defined and the template specifications supplied by the Kestrel Institute are used as shown in Figure 102 below oe StateMonad defined based on the GCDState with corresponding monadic return and bind functions type StateMon
6. 12 signature of the op declaration It is possible and recommended to combine the op and def in one declaration using the construct as show below in Figure 4 op light_changes c Color Color if c Read then Green else if c Green then Yellow else Red Figure 4 Alternative definition of light_changes An op definition may be considered a special notation for an axiom It is able to express the same logic that an axiom might express but unlike an axiom which is automatically assumed to be true and has no proof obligation a def may have associated proof obligations For precision the use of defs is encouraged over axioms d Claims Axioms Conjectures and Theorems Specware supports the three kinds of claims axioms conjectures and theorems These are all terms of Boolean type While an axiom is assumed to be true with no proving obligation conjectures and theorems are claims that must be proven through the use of op definitions and axioms Specware will automatically generate conjectures based on op declarations but the user can also explicitly create conjectures Specware does not really differentiate explicit conjectures from theorems and it handles them in the same way Potentially issues may arise when Specware interfaces with theorem provers which differentiate the two claims An example of a theorem definition is shown below in Figure 5 Conjectures and axioms are specified in the same way
7. NAVAL POSTGRADUATE SCHOOL MONTEREY CALIFORNIA THESIS SECURITY MODELING AND CORRECTNESS PROOF USING SPECWARE AND ISABELLE by Chuan Lian Koh Eng Siong Ng December 2008 Thesis Co Advisors Mikhail Auguston Timothy E Levin Approved for public release distribution is unlimited THIS PAGE INTENTIONALLY LEFT BLANK Public reporting burden for this collection of information is estimated to average 1 hour per response including the time for reviewing instruction searching existing data sources gathering and maintaining the data needed and completing and reviewing the collection of information Send comments regarding this burden estimate or any other aspect of this collection of information including suggestions for reducing this burden to Washington headquarters Services Directorate for Information Operations and Reports 1215 Jefferson Davis Highway Suite 1204 Arlington VA 22202 4302 and to the Office of Management and Budget Paperwork Reduction Project 0704 0188 Washington DC 20503 1 AGENCY USE ONLY Leave blank 2 REPORT DATE 3 REPORT TYPE AND DATES COVERED December 2008 Master s Thesis 4 TITLE AND SUBTITLE Security Modeling And Correctness Proof Using 5 FUNDING NUMBERS Specware And Isabelle 6 AUTHOR S Chuan Lian Koh Eng Siong Ng 7 PERFORMING ORGANIZATION NAME S AND ADDRESS ES 8 PERFORMING ORGANIZATION Naval Postgraduate School REPORT NUMBER Monterey CA 93943 5000 9 SPONSORING MONITORING A
8. Set Flow type MM Set Transform type ATTransaction MakeKnown Terminat ReadResourceExt WriteResourceExt Subject to Resource flow record type SRMatrix Set Flow Block to Block flow record Represents flow of information between blocks BBMatrix contains tuples depicting a Set of FlowModes between 2 blocks If a BBRecord linking 2 blocks is not found no allowable flow is allowed source is bl dest is b2 type BBRecord bl Block b2 Block fset FlowModeSet type BBMatrix Set BBRecord o oe oe oe oe oe oe oe oe Policy is preset and passed in during initialisation type Policy srm SRMatrix bbm BBMatrix type Input at Flow attran ATTransaction type InputList List Input EGER EK KIA RRR RAK KR KK OK KEK IRR OK OK KE UC ODE IE EGER DK ROL KER OU ELLER DEG e e ERKE eee e System Definition amp System Property FOR BEKK KE KKK RRR OK RAE IK OK OK RAKE RAK KR Ie DC KR OK CKOK KK OK HN OK KEK GE GKUKUK RERE KREERT Ene y type System blocks BSet systemflows MM pol Policy sysstate State 6 State contains the flows that are currently enabled for subjects and also the set of system resources oe type State atset Set Flow resrcset RSet Exported resource Re Internal resource Ri Resource R axiom propertySystemSetResource is fa sys System let intres sys sysstate resrcset fn i not
9. oe amp amp b2 in bset amp amp bl N b2 empty bl b2 oe oo System element axiom Union of the resources of all blocks equals the resource set No other resourc xists other than those is sys resources Blocks of sys resources are distinct o oe o oe oe oe axiom propertyRB is fa sys System NN sys blocks sys sysstate resrcset fn i gt exported i amp amp full sys sysstate resrcset amp amp distinctSets sys blocks AKER ERKAK OR Oe C SOR DRORGOR OR IR LOK IK RRR ERRA REAR BORK COE OR OK OR BERR REAR UE ERE RRR RL AK KARR Block to block Policy and Flows Check is based on the policy matrix specified WORK KC ERE RAR IK ORDRE OR ROK OR PRIOR ON REKE ORDER E OR OK DK DK OK OE IKK RRR DE KKK KKK RK HKALE Y 5 Retrieve allowed flows modes from block a to block b from given policy matrix oe 114 op BB bb BBMatrix a BlockId b BlockId FlowModeSet let bset bb fn i getBlockId i bl a amp amp getBlockId i b2 b in case single bset of tru theMember bset fset false gt empty 5 No other blocks exist other than those in sys blocks 6 All blocks can both read and write to themselves axiom BB FLOWS BLOCK INTERNAL ALLOWED is fa sys System a Block let bid getBlockId a in full sys blocks amp amp Write in BB sys pol bbm bid bid amp amp Read in BB sys pol bbm bid bid DEC REAR OR UE RA
10. 6 This trivial theorem will confirm that Prog counter will remain greater than 0 theorem pc_ok is fa n Nat pcProperty evaluate n proof Isa simp apply induct_tac n apply auto simp add Let def end proof This theorem is evaluate whether the inputted program is secure theorem system secure is fa n Nat property evaluate n This proof could not be complete in Isabelle It require an more in depth understanding of Isabelle proof Isa simp apply induct tac n apply auto simp add Let def end proof oe oe oe oe oe endspec 103 PAGE INTENTIONALLY LEFT BLANK 104 APPENDIX C BLP MODEL A BLP SW oe oe Example Implementation of BLP based on simple Monad Example which we created previously oo oo BLP qualifying spec import Library General type SecLabel TS label S label C label U label type SecLabel i Nat i 0 amp amp i lt 4 type ResourceName String type Resource name ResourceName label SecLabel type Subject Resourc type Object Resourc type Mode Read Write type ATTransaction MakeKnown Terminate Open Close type AccessTuple Subject Object Mode type State Set AccessTuple type Input AccessTuple ATTransaction type InputList List Input The state consists of just 1 variable 6 X State List AccessTuple which contains allowed transitions type Sys
11. EQ Equal NEQ Not Equal type Cond GT LT GE LE EQ NEQ 6 function to read from low input and assign to variable specified by LHP op read low func LHP MemoryState MemoryState def read low func var name mem state let read value read low mem state 2 in update variable var name read value Low mem state proof Isa simp end proof function to read from high input and assign to variable specified by LHP op read high func LHP MemoryState MemoryState def read high func var name mem state let read value read high mem state 2 in update variable var name read value High mem state proof Isa simp end proof 6 function to assign a value of a variable to a variable LHP op assignl func LHP RHP MemoryState MemoryState def assignl func l r mem state find out the value of the variable specified by RHP then assign the value to LHP if not variable not found just do nothing case r of VarName v gt let x find variable v mem state in case x of Some var gt update variable l var 2 var 3 oe ox oe oe oe mem state None gt mem state proof Isa simp end proof 6 function to assign an integer RHP to a variable LHP op assign2 func LHP RHP MemoryState MemoryState def assign2 func l r mem state 6 assign the value from RHP to LHP case r of VarValue v gt update variable 1 v Low mem state proof Isa simp end
12. SystemState Boolean def property s as nth will be used it is required to confirm the length 6 of the list before proceeding else Isabell f length s 4 1 s 4 2 then let stmt nth s 4 1 s 4 2 in 6 will return false only if the statement is writelow and the label of the variable is high if stmt 2 WriteLow amp amp exists fn i i 1 stmt 3 amp amp 1 3 High s 1 oe p oe then false else true else true 6 with simp this def will be added into the list of simplication rule for future proofing proof Isa simp end proof oe oe This function will run n number of line of the program The function is of recursive nature where it will recursively oe oe call itself until n 0 and the systemstate will be 6 iniitalize to the initial state subsequently transition 6 will happen until the initial n value op evaluate Nat gt SystemState def evaluate n if n 0 then initial_state else transition evaluate n 1 with simp this def will be added into the list of simplication rule for future proofing proof Isa simp end proof 6 This function checks whether the program counter is greater than 0 op pcProperty SystemState gt Boolean def pcProperty s 102 if length s 4 1 gt 0 then true else false 6 with simp this def will be added into the list of simplication rule for future proofing proof Isa simp end proof
13. T 20 21 22 23 24 25 26 J McDonald and J Anton SPECWARE producing software correct by construction Kestrel Institute ftp ftp kestrel edu pub papers specware specware jm pdf March 14 2001 Isabelle installation instructions http www cl cam ac uk research hvg Isabelle installation html November 3 2008 Y V Srinivas and R Jullig Specware Formal support for composing software in Mathematics of Program Construction Anonymous Springer Berlin Heidelberg pp 399 422 1995 Monad functional programming wikipedia http en wikipedia org wiki Monad functional programming November 3 2008 Norvell Monads for the Working Haskell Programmer http www engr mun ca theo Misc haskell and monads htm November 3 2008 Specware to Isabelle Interface Manual http www specware org documentation 4 2 isabelle interface SpecwarelsabelleInterface pdf November 3 2008 Specware 4 2 User Manual http www specware org documentation 4 2 user manual SpecwareUserManual pdf November 3 2008 T Nipkow L C Paulson and M Wenzel A Proof Assistant for Higher Order Logic Springer Verlag pp 214 2008 Isabelle documentation http www cl cam ac uk research hvg Isabelle documentation html November 3 2008 M Wenzel The Isabelle Isar Reference Manual http isabelle in tum de doc isar ref pdf November 3 2008 M Auguston and A B Shaffer Security
14. The traffic light can be modeled as a color sequence represented in a list with transition occurring from each sequence element to the next Figure 23 shows how this 27 transition is defined To test out proving on Isabelle a trivial theorem was formulated Two axioms are defined and used in the proving of the theorem define traffic light as a list type Traffic Light List Color 5 Axiom to state traffic light list is not empty and 5 traffic light list starts with Yellow axiom a0 is fa x Traffic Light null x amp amp hd x Yellow 5 Axiom to state the state changes in the traffic light list axiom a2 is fa x Traffic Light y Integer if y gt 0 amp amp y length x 1 then y is valid index nth x y 1 2 light changes nth x y else true oe oo This Theorem states that for all traffic light lists with any number of state changes the sequence of light changes is correct theorem light matches is fa x Traffic Light y Integer y gt 0 amp amp y lt length x 1 gt light changes nth x y nth x yt1 proof Isa simp using a0 a2 apply auto end proof oo oe oe oe Figure 23 Specware specification representing the transition from color to color in list and a trivial theorem The Specware specification can be translated to Isabelle specification by issuing the CTRL C TAB command in Specware specification window Figure 24 shows the
15. Value of High Input 5 Index Integer Points to next high input to read import TypeDefSpec TypeDef type MemoryStateValueTuple MemoryState Value Axion 1 Input List Index lt length input list axiom len input list is fa mem state MemoryState let inputLow mem state 2 in let inputHigh mem state 3 in inputLow 2 length inputLow 1 amp amp inputHigh 2 length inputHigh 1 proof Isa simp end proof 9 o Read from the low input list based on the current index op read inputLow MemoryState gt Integer def read inputLow mem state nth mem state 2 1 mem state 2 2 proof Isa simp using len input list apply auto end proof 9 o 5 Read from the high input list based on the current index op read inputHigh MemoryState gt Integer def read inputHigh mem state nth mem state 3 1 mem state 3 2 proof Isa simp using len input list apply auto end proof 96 oe oe Read from the low input list based on the current index Increment Index Returns the value read op read low MemoryState MemoryStateValueTuple def read low mem state oe oe oe oe let read value read inputLow mem state in let updated input stream mem state 2 1 succ mem state 2 2 in let updated memory mem state 1 updated input stream mem state 3 in updated memory read value proof Isa simp end proof oe oe Read from the high input list based on the curren
16. c SYSIOHE SCE iier ecu ERE akon einen Esa O 69 d State Mohuds iua ie eth pesetas ac Een ES 71 e SeCUrity PTCA COLES oso ti etiaai el rp as 72 Security TRCOPEINS ss svesccsescseiwassnabesvavndeguanssseveveradenebsndocesnnveseneess 75 g Partial Ordering and Trusted Partial Ordering 78 3 Discussion and Lessons Learned ceres eene 80 RESULTS AND ANALYSIS etico ebeio Aper urbo ape e epis eS pekh Pao CREDERE S be RE RES EERR e po RIDE REEF eM 83 A SPECWANRE csdprisscerisdriecevensuteVbuoeu eeepbucesWagadodvuck deese bncapoe aded Eva ie OR aeo 83 B IE BELLE reme 83 C SPECWARE TO ISABELLE TRANSLATION ee ee eene eene neno 84 D SETTING UP OF SPECWARE ISABELLE DEVELOPMENT ENVIRONMENT iiit preoske ks bebo eI o Eee bP v Cin seseo TEES CLR Un ET NEP bn Road oso eS E bE 85 E SIUS diei E EE tue cb ccsasssuhsuppsoesaabeassenins E EE ETE 85 F MONA DIS ciccseassiontevidcosscccessesdvsslesteusovetceveddarsavesisosaviedostedsntetdovsddocdsccasaeecssecetsais 85 G MPS E E E OAS E P ER QUM ANS Uu Dto DE 86 VL CONCLUSION ccsacceccatsvses cusaeddceascatua tutu ec uscadsctaisspausasecaved osn aoei S EEs Ce eS SE atea 87 A CONCLUSION 55 iieiveet secte oboe ctn ated iei earned neni 87 B FUTURE WORKS mo ietn bm A eiecti qu cc aou 88 1 Proving of the Model Using Isabelle eere 88 2 Segregation of the Model int
17. full sys blocks amp amp Write in BB sys pol bbm bid bid amp amp Read in BB sys pol bbm bid bid Figure 80 Definition of BB On completion of the discussion on flow and flow policy we are now ready to describe what a system is In the LPSK paper the following elements are used to define a System following a least privilege separation model a set of resources RSet e a set of operations O this translates to Transform in our model e a set of modes of flow FlowModeSet a partitioning of resources into a set of blocks BSet an operation to effects function MM a block to block flow function BB a subject to resource flow function SR 67 A system can thus be represented as RSet Transform FlowModeSet BSet MM BB SR In our model it is recognized that the FlowModeSet has already been defined in the model under type specification A complete description of a System will need to include both its static and dynamic elements Under static elements BSet has to be specified to define how the resources are assigned to blocks and MM to define the actualized Transform in the system BB and SR have to be furnished at system initialization in the form of a Policy object containing the BBMatrix and a SRMatrix The two matrices are initialized during system startup and remain static thereafter For dynamic element the system state State is defined This contains the flows that are currently enabled for
18. op trusted Resourc gt Boolean type ResourceExt Resource exported type ResourceInt Resource notexported Figure 68 Resource Types and Properties An active resource ResourceActive is an external resource which is active and initiates operations on a passive resource Examples of active entities of a system include a program a process or an agent In our model the type Subject is used to represent such an entity in the separation kernel type ResourceActive ResourceExt active type Subject ResourceActiv type TrustedSubject Subject trusted Figure 69 Declaration of ResoureActive Subject and TrustedSubject A trusted subject TrustedSubject is next defined in Figure 69 to be a subject that is allowed to perform operations not normally allowed for ordinary subjects by policy The concept of trusted subject being allowed to but not required to violate partial ordering is used in the discussion on Partial Ordering and Total Partial Ordering later The terms RSet ReSet RiSet and RsSet are declared next as shown in Figure 70 to represent the sets of Resource ResourceExt ResourceInt and Subject in a system respectively Set of resource type RSet Set Resourc type ReSet Set ResourceExt Set of exported resources type RiSet Set ResourceInt Set of internal resources type RsSet Set Subject SSSet of subjects Figure 70 Declarat
19. 1X THIS PAGE INTENTIONALLY LEFT BLANK Figure Figure 2 Figure 3 Figure 4 Figure 5 Figure 6 Figure 7 Figure 8 Figure 9 Figure 10 Figure 11 Figure 12 Figure 13 Figure 14 Figure 15 Figure 16 Figure 17 Figure 18 Figure 19 Figure 20 Figure 21 Figure 22 Figure 23 Figure 24 Figure 25 Figure 26 Figure 27 Figure 28 Figure 29 Figure 30 Figure 31 Figure 32 Figure 33 Figure 34 Figure 35 Figure 36 Figure 37 Figure 38 LIST OF FIGURES Spec DOPO castles ep DUM oiu s totas ace aae Pan prd co teas 11 Decl ration of Types a sos eosque ve peto dito ue eR E TRE HU vase ae a a i 12 Definition of ight changes Operation essere 12 Alternative definition of light changes seen 13 Theorem Definition in Traffic Light Model eee 13 State Monard and accompanying monadic functions esses 15 Sample Specware SPECI CAUOM gaceccetshs vescsed praedo tee hod oda RO UE 16 Isabelle specification translated from the sample Specware Specification 17 Screenshot of XEmacs for Specware and Isabelle sss 17 Example of sub goals being proven in Isabelle sess 18 Example of sub goals in Isabelle before induction is applied 19 Example of induct tac being applied to the variable n 19 Typical proof of skeleton of Isar proofs
20. CTRL F XEmacs command to open a file CTRL x CTRL S XEmacs command to save a file CTRL x CTRL c XEmacs command to close XEmacs CTRL c p Specware command to process current file CTRL c TAB Specware command to translate file to Isabelle Table 1 Common XEmacs and Specware commands C ISABELLE PROVING APPROACHES 1 Apply style Proofs An apply style proof is an interactive proof in higher order logic HOL using Isabelle s proof assistant 22 Proofing strategy can be selected using the apply function in Isabelle From the theorem sub goals are derived and have to be proved The thesis only lists a few examples of the commands supported under apply style proofs More comprehensive coverage can be found on Isabelle s website 23 a apply auto This command will adopt the proof strategy called auto to try to solve all the sub goals automatically 22 Figure 10 shows a sample output when Isabelle is able to solve the sub goals proof prove step 1 goal No subgoals Figure 10 Example of sub goals being proven in Isabelle 18 b apply induct_tac x This command will apply a proof strategy called induct_tac to perform induction to the variable x 22 Figure 11 shows an example of sub goals in Isabelle before induction is applied while Figure 12 shows an example of induct_tac being applied to the variable n proof prove step 0 goal 1 subgoal 1 propert
21. I IK RRR KC ORG op secure write transition S1 State at Flow Boolean if Write in at fset then let S write op at subj at obj S1 2 in get resource memory at obj S1 1 get resource memory at obj S 1 gt currently accessible at S1 1 else false op secure read transition S1 State at Flow Boolean if Read in at fset then let S read op at subj at obj S1 2 in get resource memory at subj S1 1 get resource memory at subj S 1 gt currently accessible at S1 1 else false op securestate S State policy Policy Boolean fa at Flow at in S atset gt access secure policy srm policy bbm at Resource contains a set of bits 6 State consists of a policy and a set of resources 120 theorem EmptySecure is fa sys System sys sysstate atset empty amp amp securestate sys sysstate sys pol theorem SecureSystem is fa S State input Input sys System securestate S sys pol gt securestate transition input sys S 2 sys pol amp amp secure_write_transition S input at amp amp secure_read_transition S input at endspec 121 THIS PAGE INTENTIONALLY LEFT BLANK 122 1 2 3 4 5 6 7 8 9 10 11 12 13 14 LIST OF REFERENCES S Ubhayakar Evaluation of Program Specification and Verification Systems June 2003 D DeCloss Analysis Of Specware
22. ResourceExt StateMonad op get resource StateMonad RSet fn S State gt S resrcset S 116 op get resource memory Resource gt StateMonad Set Bit AIO OK KOKCOK KK eo RRR KR REI KER KK CUERO OR IR ERE LA ERR RSA ERIKA LER RK SR EK Top level execution and initialisation function Transition function that transits the system state FERIA LIRA OR OK OK PECORE SR OR ORO Ce DC LAK KR KK BRAK RD BRAK OC OUI RRR RRR ACARI OR RR KB RK REE op transition Input System StateMonad Boolean def transition inp sys let policy sys pol in let at inp at in let inputtran inp attran in case inputtran of MakeKnown gt curr currently accessible at if curr amp amp access secure policy srm policy bbm at then add access at return true else return false Terminate curr currently accessible at if curr then remove access at return true else return false ReadResourceExt gt curr currently accessible at if curr then b4resourceMem lt get resource memory at subj read op at subj at obj afterresourceMem get resource memory at subj return x memsect Set Bit memsect lt b4resourceMem amp amp memsect lt at obj rscmem amp amp memsect lt afterresourceMem else return false 117 WriteResourceExt gt curr currently accessible at if curr then
23. Specware 4 2 2 Library IO Emacs There is a bug with x symbol and the latest version of xemacs and x symbol is not required to run Specware 22 Include the path to Isabelle usr local Isabelle bin to the line Isabelle p in the file Isabelle Specware in opt Kestrel Specware 4 2 2 directory To specify the path to Isabelle Table 2 List of Tasks for Specware 4 2 2 to run in Fedora 8 23 THIS PAGE INTENTIONALLY LEFT BLANK 24 IV SECURITY MODEL A MODELING STRATEGY An iterative and incremental approach as shown in Figure 18 was adopted in modeling in the project as the team is new to both security modeling and functional programming After setting up the initial environment the team built a simple Specware specification that models a Traffic Light to get familiarized with Specware as described in the next section Concepts about state and transition are incorporated in the model as a preparation for security modeling The proof obligations are subsequently discharged and proven using Isabelle The Traffic Light Model was expanded into a BLP property model as our first attempt on security modeling The team was unable to successfully prove this first simple model using Isabelle even when the model is trimmed to the bare minimal and trivial theorem is specified for proving It is found that some understanding of the intrinsic of the theorem proving in Isabelle is essentia
24. System State The set of resources defined under State can be divided into a set of exported resources and a set of internal resources The sets RiSet and ReSet are distinct and do not overlap as depicted by the set relation in Figure 83 axiom propertySystemSetResource is fa sys System let intres sys sysstate resrcset N En 1 notexported i in let exres sys sysstate resrcset N fn i gt exported i in intres exres sys sysstate resrcset amp amp intres N exres empty Figure 83 Property of Resource Set 69 It was defined earlier in Figure 75 that every resource has resource memory ResourceMemory The ResourceMemory is defined to be a set of bits Potentially the set could also be empty if the resource is not loaded by the kernel or no memory has been assigned to the resource For the model the case where there is no overlap of memory between resources as defined by propertyResourceMemoryDistinct 1s assumed 5 Memory related type Bit type ResourceMemory Set Bit type Memory Set Bit axiom propertyResourceMemoryDistinct is fa resrcl Resource resrc2 Resource resrcl rscmem N resrc2 rscmem empty resrcl resrc2 Figure 84 Definition of Memory To analyze how state changes will transition inside our model the system state needs to be defined For the purpose of our model a system state is defined to consist of a set of access tupl
25. closed results outside the scope of this thesis In conclusion through our work in this thesis we found that Specware together with Isabelle has great potential for specifying and verifying a security model They will be great tools for experienced user in the theorem proving field We hope that the illustrated use of Sets and Monads in our LPSK example will also be useful to future users of Specware B FUTURE WORKS 1 Proving of the Model Using Isabelle Isabelle is an interactive theorem prover with lots of capabilities that had yet to be explored in this thesis Further studies may be performed to understand the various approaches in theorem proving using Isabelle and the pros and cons of each approach With the understanding of each theorem proving approach a complete proof for the LPSK model could be explored 2 Segregation of the Model into an Abstract Canonical Model and a Refined Model No conscious effort has been put in when specifying the LPSK model to first create an abstract model which is subsequently refined Work could be done to segregate a reusable canonical abstract model from the current specification Refinements to the 88 model can also be supported with Specware s morphism features to specify a concrete level representative of the LPSK API and functional behaviour 3 Code Generation from a Verified Model using Specware Code generation is one of the capabilities of Specware It is known that infinit
26. interactive theorem prover with automatic proving capability where the user needs to have substantial 83 knowledge and experience in logical calculus to complete a proof Although Isabelle provides a very extensive list of documentation most of the documentation assumes a strong background and experience in proof logic An introductory guide with illustrated examples on how proving strategies and how proving may be guided interactively in Isabelle would be most useful for beginners Auto proving in Isabelle succeeds only for simple and trivial theorems as experienced by the team Proving becomes more manual when the theorems become more complicated Subtheorems could be added as intermediaries for guiding the proofs Isabelle has a large user group with two mailing lists a user mailing list and a developer mailing list The mailing lists will be useful for beginners to post questions and learn from developers and fellow users It is noted though that answers are provided only out of goodwill and it is not guaranteed that responses will be received upon posting of questions to the forum Still it will be extremely useful for beginners to learn from past queries posted by others C SPECWARE TO ISABELLE TRANSLATION Although Specware to Isabelle translation is considered as an initial experimental release 20 it provides an almost seamless translation from Specware specification to Isabelle specification using the Specware to Isabel
27. is still very much restricted to the academic and military fields Although it is not all about complicated mathematics it requires a paradigm shift from normal software engineering Depending on the support tools chosen the learning curve is not trivial and experience is critical to develop a good formal specification Proper training is required for formal methods practitioners The success of a formal method application is very much dependent on the quality of the practitioners 8 Formal methods could be broadly categorised into three groups refutation verification and intensive mathematical study of key programs each with its own strengths weaknesses and costs 8 In refutation as is employed in the Alloy Aanlyser one tries to refute the claim that the specification meets its requirements by searching for counterexamples It is based on the small scope hypothesis which states that if an inconsistency in a model exists there is a high probability that it will present itself within a small scope of the model The finding of counterexamples is not absolute proving in the strictest sense although the finding of one counterexample is enough to conclude that a particular system is insecure Often model checking may be slow as it runs extensively in the searching of counterexamples Verification attempts to provide a basis by which software can be proved to be a correct realization of its specification Typically this is only car
28. manipulators of Current ACCESS esee 53 State Transition eee a s a E 54 Theorem Brnplby 1S 36 Ie oso o epi t p Ui ront eed eae 55 Sub theorems for Make Kno WI tetti Ett bete eoi d ev ta bid ecd gea deus 25 Sub theorem for Terminate aceite et treat ete daba ede idco 55 Theorem Transition State SeGUEE aei eee eei uneciide au edit iesas 56 Resource Types and Properties a ates cased cada opt redu lat iocus 59 Declaration of ResoureActive Subject and TrustedSubject 59 Declaration of Resource Sess ee ten ato ed 59 Declaration of Block dnd BSQqUos suite casts cunt haw aod reb rt dia 60 Blocks Gf ResoUutcesa uie Receta D eda ced ebd De sr bdg e 61 TheR so rce BU secret nics tte cing oi en dc tI wed rie e eee 61 Proper OL OCR oai constr Nontetul dd bles cana DIU a diualead scene Da NN CON 62 Declaration of a Resource a eo Et oM eti adus 63 Definition of Block and related operations eseeeee 64 Definiton of Flow FlowEffect Transform and MM eR 65 Definition ol POHCyY Au o oecsxode ene indicada Rb ge oops ens abs eri atus 65 IDENT ONO SRMaIUIX eene is stu qosistutus sa ee ated ge eae 66 Definition of BB de 67 Definition of System and SUle ou oit ciues arts ti eee tase ce dequo eis tes ERE RNRE 68 System Components and their Relationships eese 69 Property of Resource Set e eei poii ta prse UA Scire cotes 69 Figure 84 Figure 8
29. may sometimes result in a translated Isabelle Specification which is harder to prove When this happens it is always recommended to use the if then else construct instead In summary the team discovered more undocumented features in Specware and Isabelle such as the ceiling limitation of the number of elements supported in a Specware 45 type product type The security model was built and the proof was discharged to Isabelle It was found that the proof could not be completed automatically using the simp and auto rules although very trivial theorems were constructed Posts were made to the Isabelle user group but no response was obtained It was not easy to discern if the problem arises due to inherent inadequacies in the model the translation performed by the Specware Isabelle Interface or just technicalities and know how of guiding Isabelle in its proof With limited time and resources it was decided that a trip would be made to Kestrel to seek first hand technical advice on the model D LESSONS LEARNED AT THE KESTREL INSTITUTE The visit to the Kestrel Institute was made with the following objectives e to seek advice and guidance in proving using Isabelle to clear doubts on the interface between Specware and Isabelle to reconfirm our modeling approach and to verify the correctness in our use of the newer and not well documented features of Specware The initial version of the BLP specification described in the next s
30. model in Alloy Thanks to Monique Cadoret for editing our thesis We also wish to thank our sponsors the Defence Science amp Technology Agency DSTA and ST Electronics Limited for enabling and supporting our participation in this valuable program at the Naval Postgraduate School Last but not least thanks to our families and friends here in Monterey and in Singapore for their moral support It is their encouragement that keeps us going xvii THIS PAGE INTENTIONALLY LEFT BLANK xvili I INTRODUCTION Developing a high assurance system requires the building of a security model that is verified using formal methods Theorem provers and model checkers are some of the formal method s tools that help to build specifications for a security model and mathematically verify their correctness Former NPS students have explored various formal specification tools such as PVS 1 Specware 2 and Alloy 3 for their usefulness in formally specifying a security model to represent security policies and verify their correctness In this thesis we are revisiting Specware an automated software development system 4 by Kestrel institute It exploits category theory to capture the refinement of specifications into code and the composition of software components In DeCloss s thesis 2 it is mentioned that the Snark automated theorem prover bundled with Specware is deficient in multiple ways including insufficient logging ca
31. proof function to get value from variable name if variable not found zero will be returned by default op get var value Name MemoryState Value def get var value n mem state let x find variable n mem state in case x of Some v gt v 2 6 default to 0 if not found oe oe o oe 98 None gt 0 proof Isa simp end proof Evaluate the conditional statement This function is not used can be used in future to expand this o oe o oe work oe oe the if then else statement can be represented using case version 4 2 2 has some problem with conversion of case statement in some instance that why if then else is use This issue should oe oe oe oe be oe resolved in version 4 2 5 op cond eval LHP RHP Cond MemoryState Boolean def cond eval l r cond mem state case r of VarName v gt let x get var value 1 mem state in let y get var value v mem state in if cond GT then x gt y else if cond LT then x lt y else if cond GE then x gt y else if cond LE then X lt y else if cond EQ then 26 ire v Y else if cond NEQ then a x Sy 5 default true else true VarValue v gt let x get var value 1l1 mem state in let y v in if cond GT then x gt y else if cond LT then x lt y else if cond GE then x gt y else if cond LE then iS y else if cond
32. shown in Figure 2 11 oe type Color oo changes type Define that color can be Red Yellow or Green Red Yellow Green Define that Traffic lights is a color and integer tuple The integer acts as a counter to indicate the number of state raffic Light Color Integer C An operation or op in MetaSlang is a syntactic symbol accompanied by a Type It is used to describe instantiations of types An op may be used to declare explicit types as well as declare functions performing an operation based on the types given in the declaration Examples of op declarations are show in Figure 3 An op can be either monomorphic or polymorphic as shown by the examples ight changes and map respecitively Figure 2 Declaration of Types Ops and Defs oe oe oe oe op oo CAC oe oe op Example of monomorphic op Declaration of light changes light changes Color Color Definition of light changes def light changes c if c Red then Green else if c Green then Yellow else Red Example of polymorphic op in List sw map a b a gt b gt List a gt List b def map f 1 case l of gt tL hd tl gt Cons f hd map f tl Figure 3 Definition of ight changes Operation The behavior and constraint of an op may be further quantified with a def definition An op definition corresponds to a previously declared op and must match the
33. team proceeded to build a model of the TCX LPSK using monadic state representation and transition based on the security model which that has been created in the preceding experiments Flows between subjects and objects are modeled as state changes The implementation is performed using the latest release of Specware version 4 2 5 which was made available to us after the visit to Kestrel in November 2008 This version incorporated the new Set Base Library which we found to be useful in the representation of relationships among the various entities in the model 2 Specware Model a Resource and Block Type Resources are defined to be the totality of all hardware firmware and software and data that are executed utilized created protected or exported by the separation kernel 12 Resources can further be subtyped into exported resources and internal resources Exported resources ResourceExt refer to resources including subjects which can be explicitly referenced via the separation kernel interface Conversely internal resources Resourcelnt are those which are only available to the kernel and to which explicit reference is not possible The predicates exported notexported active and trusted are declared to define which resource is exported internal active and trusted respectively as shown in Figure 68 58 op exported Resourc gt Boolean op notexported Resourc gt Boolean op active Resourc gt Boolean
34. to bb getBlockId i getBlockid i Qh Qh Antisymmetric 118 direct flow to bb getBlockId i getBlockId j amp amp direct flow to bb getBlockId j getBlockid i gt i j amp amp Transitive o9 direct flow to bb getBlockId i getBlockId j amp amp direct flow to bb getBlockId j getBlockId k gt direct flow to bb getBlockId i getBlockId k oo oo BBMatrix contains a set of BBRecord record block block flowset We would like to extract out the allowed flows from this bearing in mind that a flow is a tuple consisting of a subject object fmode op derivebbflowset bbm BBMatrix Set Flow let setsetflow map bb2flowset bbm in setsetflow o oe oe oe oe oe op bb2flowset bb BBRecord Set Flow let blsubject bb bl fn i gt active i in let b20bject bb b2 in let bbduple blsubject b20object in map fn a b gt subj a obj b set bb fset bbduple ARE IE ER ER AOE ARK OKUKUK REN RK IR ORG REI REI AS RIOR RI RRR ROKK EIS KK ER FORK AER AR Trusted Partial Ordering of BB Bbase Trusted partial ordering for system Trusted Subject is a Subject that has undergone rigorous analysis amp is trusted not to downgrade information other than the information it is intended to downgrade He is allowed but not required to violate the partial ordering Flows will exist in the System that will violate the pa
35. translated Isabelle specification 28 types Traffic_Light Color list consts light_changes Color lt Rightarrow gt Color defs light_changes_def light_changes c lt equiv gt if c Red then Green else if c Green then Yellow else Red axioms a0 lt not gt null x lt and gt hd x Yellow theorem a2_Obligation_subtype lt lbrakk gt y int lt ge gt 0 y lt int length x 1 lt rbrakk gt lt Longrightarrow gt y 1 lt ge gt 0 by auto theorem a2_Obligation_subtype0 lt lbrakk gt y int lt ge gt 0 y lt int length x 1 y 1 lt ge gt 0 lt rbrakk gt lt Longrightarrow gt y 1 lt int length x by auto theorem a2 Obligation subtypel lt lbrakk gt y int int length x 1 y lt ge gt 0 lt rbrakk gt lt Longrightarrow gt y lt int length x by auto axioms a2 if y lt ge gt 0 lt and gt y lt int length x 1 then x nat y 1 light changes x nat y else True theorem light matches simp lt lbrakk gt y lt ge gt 0 y lt int length x 1 lt rbrakk gt lt Longrightarrow gt light_changes x nat y x nat y 1 using a0 a2 apply auto done Figure 24 Translated Isabelle specification for transition from color to color in list and the trivial theorem Proving can be done in Isabelle by using the Retract Undo Next Use or Goto commands as shown in Figure 25 The Retract command wil
36. x86 linux tar gz tar C usr local xzf HOL x86 linux tar gz Normally the default settings of Isabelle should be sufficient for invoking Isabelle Proof General like this usr local Isabelle bin Isabelle p xemacs Failure on this is typically a problem with bad Emacs versions the command line option p specifies a different Emacs executable usr local Isabelle bin Isabelle p emacs22 The X Symbol package is already included in Proof General but needs to be enabled separately use the x command line option or the Options menu If all fails Isabelle may also be run without Proof General via the plain tty interface as follows using CTRL D to exit usr local Isabelle bin isatool tty The above x86 binaries may be also used for 64bit Linux but are restricted to 32bit mode native x86 64 platform support requires manual compilation of Isabelle Warning Pre packaged versions of Isabelle Proof General and Poly ML floating through the Net as deb rpm port etc are often outdated and rarely work as advertized Even XEmacs is better compiled manually these days the packages provided for SuSE Ubuntu and Debian are mostly broken Figure 16 Installation Instruction of Isabelle 2008 From Ref 16 3 Specware Version 4 2 2 Execute setuplinux bin that comes with the Specware version 4 2 2 installation package to install the Specware software Figure 17 shows a possible xcb_xlib error you may encounter while ins
37. 4 Proving Using Isabell uesedidss ee nostr resa r rana neo v4 oa eat ta Fev dean eo 48 E MODELING BLP IN SPECWARE esee ee eee eee ease ta seen sete seen setae 49 1 Model Description seesseessececosscooesosoesseoosssoscoseccocessossocossssecossessssose 49 2 Spec ware MOE D 50 a Required LADO ci cls cider iui eins rst ori de eae etnies 50 b TYPO DOSCTIDUON sscdessavssedsisidcxsas Beason Boni OR aaa nd Pee conto 50 e Transactiolis n oie recie tp otis si csie sikeso 50 d Input veinna iea CUNEO ROI ELENE CRDV ONE DU HN 51 e DALE doo E RUN QR E adu i RUP Sa tastes Pac teme 51 f Security Property eee enieisis e siecs etse b bene orna ous p Erogo y ervh es 52 g State Transition Transformation eee eres esee eene enne 53 h Theorems aee aos rar aveva eX VOR SERERE EVA i YER E eas 54 i Proving in Isabell ssscsssicsssscasisssisssssncavcexenevenusnsvonansvgunvevshavesenss 56 3 Discussion and Lessons Learned eere eene 56 F MODELING LPSK IN SPECWARE eee eee eee enata seen seres eto setae 57 1 Model Description sesesssooesssoocsssosecsssscccssssocesssoocsssoseesssscossssoossssose 57 2 Sp cware Model sississsosisiissisoiesescsscsosestodospa sao tese osasto osssiosooses sioba isee 58 a Resource and Block Type sscccsssccssssscssrscssssccssscccssscssessceees 58 b PLOW S ecc t iit ies detti aee ctu aaa struc tied 64
38. 5 Figure 86 Figure 87 Figure 88 Figure 89 Figure 90 Figure 91 Figure 92 Figure 93 Figure 94 Figure 95 Figure 96 Figure 97 Figure 98 Figure 99 Figure 100 Figure 101 Figure 102 Figure 103 Figure 104 Figure 105 Defi ition ob MOIOLY2 eoo aN i a a ia elitas 70 Different types defined in ATTTransaction eeeeeeeeeeenet 71 State Monads for state access and modification sess 72 Securty TAT IC ale Soon Civ oe v edt e i HN BORN ER QNM NER UE 73 Definition of transition operation cesses enne enne 75 Encapsulating fUncCtlonD uec cst eed nera Y een ANY RUCRAT ease ESI EXER Sce EE aa 76 Security Theorems for secure state ases con porro PU eI ii use ipo ode rRua ere YE Definition of Partial Ordering o coo osdbi ties geek ero Der MB HN UNE ARE INE 78 Definition of op to extract flows from BBMaatrix eee 79 Definition of Trusted Partial Ordering eee 80 if then else CONS WUC Dou ose ede e o eoe Mie aah de eee uds 82 Chained predicate CONSUME scuassasess ba ense besstofa Torqadeds cea a EN lebunewd 82 Euclid s Algorithm for calculating GCD eee 9 Declaration Of STate os aa emet aout et E T ELA tones snes 9 State Transformers for accessing and changing the State 91 Haskell SpectfICablOni aspeteseeestae eva coste teo uas iere ce ems tbe ee esdpvese defe aE 92 Encapsulating GCD funct
39. And Its Usefulness In The Verification Of High Assurance Systems June 2006 D A Phelps Alloy Experiments for a Least Privilege Separation Kernel 2007 Welcome to specware http www specware org November 11 2008 Isabelle http isabelle in tum de June 11 2008 J M Wing A Specifier s Introduction to Formal Methods IEEE Computer Vol 23 pp 8 26 September 1990 A Hall Seven Myths of Formal Methods IEEE Softw Vol 7 pp 11 19 1990 D M Berry Formal methods the very idea Some thoughts about why they work when they work Science of Computer Programming Vol 42 pp 11 27 January 2002 Common criteria documentation http www commoncriteriaportal org November 20 2008 R S Sandhu Lattice Based Access Control Models Computer Vol 26 pp 9 19 1993 J M Rushby Design and verification of secure systems in SOSP 81 Proceedings of the Eighth ACM Symposium on Operating Systems Principles pp 12 21 1981 T E Levin C E Irvine and T D Nguyen A least privilege model for static separation kernels Naval Postgraduate School Monterey CA Tech Rep NPS CS 05 003 http cisr nps edu downloads nps cs 05 003 pdf 2004 J H Saltzer and M D Schroeder The protection of information in operating systems in Proceeding of IEEE pp 1278 1308 1975 Specware documentation http www specware org doc html October 31 2008 123 15 16 17 18 19
40. EQ then x y else if cond NEQ then xX y 5 default true else true proof Isa simp end proof endspec 99 D INITSPEC SW oe oo oe oe Init spec import TypeDefSpec TypeDef op initial state SystemState def initial state SystemState init Variable x 0 Low ey 0 Low init low input 2 7 18 0 init high input 10 35 0 init program sO Assign2 si ReadLow s2 Assignl s3 ReadHigh n T 4 o9 o9 o oe A o o oe s4 WriteHigh s5 WriteHigh s6 Stop 0 proof Isa endspec simp E oe oe oe oe the property of BLP This specification wil oe oe end proof FILESYSTEMSPEC SW VarValue 5 VarValue 0 VarName VarValue 0 VarValue 0 VarValue 0 VarValue 0 y This Specification is where the program initial state and list of statement is defined This the the main specification file modeling the l require the following oe ove Specware files TypeDefSpec sw StatementSpec sw InitSpec sw MemorySpec sw System spec oo oe oe oe oe oe oe oe Fil 6 import th required Specwar import TypeDefSpec TypeDef import StatementSpec Statement import InitSpec Init 6 system state transition op transition def transition s if length s 4 1 let vars s 1 in let inputLow s 2 in let inputHigh s 3 i
41. ER AER AR Type Definitions KER EE ERRER KEK KERIO OC OK KK c eoe LON oc KERERE KEEKEEKE K E IORI IE KER KEE IORI wee vs KER RAR type ResourceId String 5 Identifier for block type BlockId 5 Resource type Resource rscid ResourceId blkid BlockId rscmem ResourceMemory op exported Resourc gt Boolean op notexported Resourc gt Boolean op active Resourc gt Boolean op trusted Resourc gt Boolean type ResourceExt Resource exported type ResourceInt Resource notexported type ResourceActive ResourceExt active type Subject ResourceActiv type TrustedSubject Subject trusted 5 Set of resource type RSet Set Resourc type ReSet Set ResourceExt Set of exported resources type RiSet Set ResourceInt Set of internal resources type RsSet Set Subject Set of subjects oe Partitioning of resources into blocks Block is a set of Resource type Block Set ResourceExt 5 set of blocks type BSet Set Block Memory related type Bit type ResourceMemory Set Bit type Memory Set Bit 111 Flow related type ModeOfFlow Read Write type FlowModeSet Set ModeOfFlow Flow effect amp Set of all possible flow effects HA type Flow subj Subject obj ResourceExt fset FlowModeSet Defines all effects associated with an operation transform type Transform
42. GENCY NAME S AND ADDRESS ES 10 SPONSORING MONITORING N A AGENCY REPORT NUMBER 11 SUPPLEMENTARY NOTES The views expressed in this thesis are those of the author and do not reflect the official policy or position of the Department of Defense or the U S Government 12a DISTRIBUTION AVAILABILITY STATEMENT 12b DISTRIBUTION CODE Approved for public release distribution is unlimited 13 ABSTRACT maximum 200 words Security modeling is the foundation to formal verification which is a core requirement for high assurance systems This thesis explores how security models can be built in a simple and expressive manner using the Metaslang specification language in Specware The models are subsequently translated via the Specware to Isabelle Interface to be proven for correctness in Isabelle which is a generic interactive theorem proving environment It is found that the translation between Specware and Isabelle is almost seamless and there is much potential in the use of Isabelle HOL to discharge proof obligations that arise in developing Specware specifications although the actual proving requires substantial knowledge and experience in logical calculus 14 SUBJECT TERMS Formal Method Theorem Prover Monads Specware Isabelle LPSK 15 NUMBER OF PAGES 146 16 PRICE CODE 17 SECURITY 18 SECURITY 19 SECURITY 20 LIMITATION OF CLASSIFICATION OF CLASSIFICATION OF THIS CLASSIFICATION OF ABSTRACT REPORT PAGE ABSTRACT Unclassified Unclassifi
43. In particular a formal security policy model is concerned with the security of the system A specification is abstract and specifies what is to be done instead of how it is done It specifies only whatever level of detail is necessary leaving unsaid what is deemed unimportant A specification is central to a project and proofs of the specification s properties are at least as useful as proofs of correct implementation The formal specifications are proven to satisfy the mathematical model Formal methods can be employed in any stage of system development from requirement specification to design implementation testing and maintenance right up to 3 verification and evaluation although cost and return of value may differ for each stage It is useful in unravelling ambiguity incompleteness and inconsistency in the system increasing the correctness of the system Applying formal methods can benefit many areas in addition to security including fitness for purpose maintainability ease of construction and better visibility 8 Most formal methods have not been applied to specifying large scale software or hardware systems Hence most are still inadequate to specify many important behavioural constraints beyond functionality e g fault tolerance real time performance and human factors There is also a general lack of integration between formal methods with the entire system development effort The application of formal methods
44. K ARK K COGOR ARR BERK COGOR E OK CK OK DK OC OK COE KR BRK REAR EIR IK OK TK KR UK KE CR RU Subject to Resource Policy and Flows Check is based on the policy matrix specified EEK OK OKOK KR KA RRR RAK KAR OR OK OE KRABI EKA ECKE OR KORR OK OK OK RE E OK CK OK ECKE OK GEO OR RRR e e e ERER KY oe returns the modes of flow allowed between a given subject and resource in a given SRmatrix op SR pol SRMatrix subj Subject extobj ResourceExt oe FlowModeSet let bset pol N fn i gt i subj subj amp amp i obj extobj in case single bset of tru theMember bset fset false gt empty axiom SRSingleEntrySubjObjPair is fa pol SRMatrix subj Subject extobj ResourceExt let bset pol N fn i gt i subj subj amp amp i obj extobj in single bset empty bset Checks if a specific mode of flow between a given subject and resource is in a given Transform op flow occurs t Transform f Flow m ModeOfFlow Boolean m in f fset amp amp f Xn op access allowed SRMatrix BBMatrix Subject ResourceExt FlowModeSet gt Boolean def access allowed srm bbm subject object am am lt SR srm subject object amp amp am lt BB bbm subject blkid object blkid op access secure SRMatrix BBMatrix Flow gt Boolean def access secure srm bbm subj subject obj object fset am access_allowed srm bbm subject o
45. ND A FORMAL METHODS MODELS AND VERIFICATION Formal methods are as described by Wing 6 mathematically based techniques to describe system properties A method is formal if it has a sound mathematical basis and this provides the means to precisely define notions like consistency and completeness and more relevantly specification implementation and correctness typically using a formal specification language Formal method provides the means to prove properties of a system without necessarily running it to determine its behaviour that a specification is realizable and that a system has been implemented correctly A formal model is one constructed from requirements and informal rules and policies on the system It is a precise and unambiguous statement of a system s security policy For example for a security model mapping is performed to map a security policy to a mathematical model It is then informally argued that the model is consistent with the security policy If the model is an accurate restatement of the policy and if the model is self consistent we can conclude that the policy is self consistent A formal specification refers to the specification for a created formal mathematical model Formal Model It is a precise definition of what the software is intended to do 7 It differs from conventional design specifications in that it is concerned only with the function of the system and makes no commitments to its structure
46. Stop Left hand part type LHP Name Right hand part type RHP VarName String VarValue Integer used to indicate the index for next statement to execute normally first ProgCounter is used but when conditional statement like if then else is used the first ProgCounter is for positive evaluation in if and the second ProgCounter is for the negative evaluation in else type NextProgCounter ProgCounter ProgCounter 6 Statement declaration type Stmt Name TypeOfStmt LHP RHP NextProgCounter 9 o Program declaration type Program List Stmt ProgCounter 5 Memory State declaration Variables Low Input High Input type MemoryState Variables Input Input 95 System state declaration Variable Low Input High Input Program type SystemState Variables Input Input Program endspec MEMORYSPEC SW oo oe This specification contains all the functions required for manipulation of Memory state variable high input and low input MyMemory spec oe oe Memory State contains of 3 components 1 Variables List of Variable 5 Variable Tuple with 2 fields Name String Name of Field 5 Value Integer Value of Field 2 InputLow List of Low Values SS Value Integer Value of Low Input 1 Index Integer Points to next low input to read 3 InputHigh List of High Values 5 Value Integer
47. URITY MODELING AND ANALYSIS The thesis demonstrates different ways in modeling BLP and LPSK using Specware and attempts to verify the correctness using Isabelle State transitions modeled using recursive function and state monads are explored Two types of proofing approaches apply style proof and structured Isar proof in Isabelle are also explored THIS PAGE INTENTIONALLY LEFT BLANK IIl OVERVIEW OF SPECWARE AND ISABELLE A SPECWARE DESCRIPTION Specware is a tool used for building and manipulating a collection of related specifications It is a design tool a logic tool a programming language and at the same time a database storing and manipulating collections of concepts facts and relationships It can be used to develop domain theories develop code from specifications and also for reverse engineering to derive a specification from existing code 14 It uses notions and procedures based on category theory and related mathematics to manipulate specifications 15 Composition and refinement are the core techniques of application building in Specware Complex specifications can be composed from simpler ones and concrete specifications may be refined from abstract ones Through refinement a more specific case of a model is built 17 Specware is designed with the idea that large and complex problems can be specified by combining small and simple specifications The problem specifications may be further refined into a working s
48. VarName v gt let x find variable v mem state in case x of Some var gt update variable l var 2 var 3 mem state oe oe oe oe oe oe None gt mem state proof Isa simp end proof Figure 43 op assign func definition The assign2 func definition uses the case method to extract the value from RHP as shown in Figure 44 and updates the variable using update variable in MemorySpec sw accordingly 5 function to assign an integer RHP to a variable LHP op assign2 func LHP RHP MemoryState gt MemoryState def assign2 func l r mem state 5 assign the value from RHP to LHP case r of VarValue v gt update variable 1 v Low mem state proof Isa simp end proof Figure 44 opassign2 func definition The get var value definition uses the find variable in MemorySpec sw to get the value of the variable if the variable is not found zero will be returned Figure 45 shows the definition of get var value 40 oe function to get value from variable name if variable not found zero will be returned by default op get var value Name MemoryState Value def get var value n mem state let x find variable n mem state in case x of Some v gt v 2 5 default to 0 if not found oo proof Isa simp end proof Figure 45 op get var value definition d Initialize Specification InitSpec sw The initialize specification contains the initial st
49. ad a GCDState gt a GCDState op a return x a StateMonad a fn st gt x st op a b monadBind ml StateMonad a f a StateMonad b StateMonad b fn st gt let y stl ml st in f y stl oe oe Figure 102 Declaration of Monads and Monadic Function State Monadic functions are defined to retrieve both X and Y and also to update X and Y as shown in Figure 103 Retrieving X and Y value op getX StateMonad Nat def getX fn x y x x y op getY StateMonad Nat def getY fn x y gt y x y Updating X and Y values op putX Nat gt StateMonad def putX input fn x y gt O0 input y op putY Nat gt StateMonad def putY input fn x y gt O0 x input Figure 103 X and Y Manipulators Finally the gcdST core function which does recursive calculation of the greatest common divisor is defined in Figure 104 Note that the sequenced calculations are encapsulated inside the gcdS T operation 93 oe State Transition function gcdST which calculate and update the values of X and Y op gcdST StateMonad Nat def gcdST oe x getX y lt getY if x y then 5 Passing back the final result return X else 5 Recursive call if x and y not equal if x y then putY y x gcdsT else putX x y gcdsT Figure 104 State Transition Function gcdST Finally the encapsulating op
50. ange transition is represented in Specware The op next state defines the state transition the op run_traffic executes the state transition the inputted number of steps 31 and the theorem ight matches is formulated just as a simple illustration of the use of apply simp add in Isabelle Figure 30 shows the translated Isabelle specification of this model Define that Traffic light is a color and integer tuple 5 The integer act as a counter to indicate the number 5 of state changes type Traffic Light Color Integer 5 Define next state function 5 This basically is representing a state transition process where the light will transit to the next light and 5 the counter will increment by one next state Traffic Light gt Traffic Light def next state x light changes project 1 x project 2 x 1 oo oe Define run traffic function This function will execute the inputed natural number count of state transition op run traffic Nat gt Traffic Light def run traffic n if n lt 0 then Yellow 0 else next state run traffic n 1 oo oe oe oo oe This theorem is trying to verify that for all traffic light light change is equal to next state theorem light matches is fa x Traffic Light light_changes project 1 x project 1l next state x proof Isa apply simp add light changes def next state def end proof oo oe Figure 29 Traffic light model
51. as productive we learned and tackled the frequent problems encountered together We found that with a translator to Isabelle Specware has become more complete as a verification tool The XEmacs environment that integrates both Specware and Isabelle is simple allowing the developer to become familiar and comfortable with both Specware and Isabelle in a relatively short period of time which is an improvement over the earlier version of Specware that DeCloss used in his thesis 2 MetaSlang the specification language in Specware is a simple and expressive language MetaSlang can represent state transition either as a history list that can be processed recursively or as a state Monad The representation of Monads in MetaSlang is very similar to Haskell a popular functional programming language and therefore should 87 be easily understandable by someone that is familiar with functional programming However for a beginner it requires a substantial amount of effort to understand and use them We have documented our understanding of Monads in this thesis in hopes of smoothing the learning curve for Monads It was found that the translation between Specware and Isabelle is almost seamless and that there is much potential in the use of Isabelle HOL to discharge proof obligations that arise in developing Specware specifications The actual proving using Isabelle requires substantial knowledge and experience in logical calculus which put
52. at AccessTuple StateMonad Boolean fn S State gt at in S S op addAccess at AccessTuple StateMonad fn S State gt O0 S at op removeAccess at AccessTuple StateMonad fn S State gt 0 S at oe oe This corresponds to the main function performing the statement It will read in the next statement perform it and then call next monad transition is a fn State Nat State straightforward if property is checking based on the state variables o oe oe o oe oe oe oe op property State gt Boolean def property s securestate s proof Isa simp end proof op transition Input gt StateMonad Boolean def transition at input transaction case input transaction of MakeKnown gt curr currently accessible at if curr amp amp access secure at then addAccess at return true else return false Terminate curr currently accessible at if curr 106 then removeAccess at return true else return false op evalProgram InputList gt StateMonad List Boolean def evalProgram inputs case inputs of gt return inp r inputs rl transition inp res evalProgram r inputs return rl res theorem EmptySecure is securestate empty proof Isa by auto simp add BLP securestate p def end proof theorem transition Terminate subset eq is fa S State S State at Ac
53. ate definition which can be replaced subsequently by any program pseudo code of the same syntax Figure 46 shows the sample initial state definition used in this thesis op initial state SystemState def initial state SystemState init Variable x 0 Low yt 0 Low r init low input 2 7 18 0 nit high input 4 10 35 0 oec oo oe p o9 o9 o9 oe init program s0 Assign2 x VarValue 5 Lj 335 sl1 ReadLow y VarValue O0 2 2 s2 Assignl x VarName y 3 3 s3 ReadHigh y VarValue O0 4 4 s4 WriteHigh y VarValue 0 Br 5 rs s5 WriteHigh x VarValue 0 6 6 s6 Stop VarValue O0 6 6 0 proof Isa simp end proof Figure 46 Sample op initial state definition e Main Specification FileSystemSpec sw The main specification of the model contains the definition state transition property checks and the theorems Figure 47 shows part of the transition definition the 41 full definition is available in the Appendix B The transition definition will go to the statement specified by the ProgCounter and based on the TypeOfStmt execute the different if then else branches After executing the statement transition will return the next system state WriteLow and WriteHigh statements are handled in the transition but since there is no output in this model it will just transit to the next sta
54. ation for the traffic light modeled as a tuple of color and the number of state changes esee 33 Computer system block diagram eese 34 Initial type declaration easi red ea epu cer EE en nee 35 Label type declaratloD odore tA dl de acest tee fees 36 Matrables type deelaratioti does Ceobedte esie vedrai Dec buph nad eso dete Raga 36 Input type declaratiom eei oae eet dei ie tal Gide 36 Type of statement type declaration ooi togae cili iet deceives 36 Statement type declaration noiae traite Poet pad eb pha ETA 37 Program Memory State and System State type declaration 37 xi Figure 39 Figure 40 Figure 41 Figure 42 Figure 43 Figure 44 Figure 45 Figure 46 Figure 47 Figure 48 Figure 49 Figure 50 Figure 51 Figure 52 Figure 53 Figure 54 Figure 55 Figure 56 Figure 57 Figure 58 Figure 59 Figure 60 Figure 61 Figure 62 Figure 63 Figure 64 Figure 65 Figure 66 Figure 67 Figure 68 Figure 69 Figure 70 Figure 71 Figure 72 Figure 73 Figure 74 Figure 75 Figure 76 Figure 77 Figure 78 Figure 79 Figure 80 Figure 81 Figure 82 Figure 83 op VAG Joyce ROTE oid teeetebr p col ec odetb anata aeaandoneannctuaseresaeeeaauees 38 op find _variable detto eec rdots odo aie art n No Edd Ra RED om ERE 38 op update variable definition eese esee enne enne 39 op read _low _ func definition seta cue peer ee PER GR ROO RN D ERR ES 39 op assign func
55. axioms 30 proof prove step 1 using this null x amp hd x Yellow if lt y amp y int length x 1 then x nat y 1 light changes x nat y else True goal 1 subgoal 1 O lt y y lt int length x oder gt light changes x nat y x nat y 1 else True theorem light matches simp lt lbrakk gt y lt ge gt 0 y lt int length x 1 lt rbrakk gt lt Longrightarrow gt light changes x nat y x nat y 1 using a a2 Mj apply auto M ne end Figure 27 After the two axioms are applied Isabelle only need to prove one subgoal Proof The theorem light_matches is proved using apply auto theorem light_matches 0 lt y y lt int length x 1 gt light changes x nat y x nat y 1 else True theorem light matches simp lt lbrakk gt y lt ge gt 0 y lt int length x 1 lt rbrakk gt lt Longrightarrow gt light changes x nat y x nat y 1 using al a2 M state apply auto M done end Figure 28 Isabelle proof for theorem light_matches for traffic light represented using list of color 4 Traffic Light as a State Tuple The traffic light can alternatively be modeled as a tuple representing the current Each tuple is comprised of a color and a counter indicating the number of transitions which have occurred from initialization Figure 29 shows how this state ch
56. bject am 115 RR RAR KRONA SED ECKE DIC SID IK IRA SRN AER KRA RRR IK IR KR ER KEKEE GE OK IE IR ELA FORE oe System state functions State Monads for accessing and changing the state variables REEK EREEREER RARER BRK BRK SKK HOOK A BRK KEREK BLK IRR BARK KE BERK BARI AERIS FERN op get_access_by_at at Flow StateMonad Set Flow fn S State gt S atset fn i gt i subj at subj amp amp i obj at obj S 6 Access Functions to retrieve and set values inside states op currently accessible at Flow StateMonad Boolean curr get access by at at return single curr amp amp at fset lt theMember curr fset op add access at Flow StateMonad curr get access by at at if single curr then remove_access at curr at get current access put current access curr at subj at subj obj at obj Fset theMember curr fset at fset return else return op remove_access at Flow StateMonad fn S State gt 0 atset S atset fn i gt i subj at subj amp amp i obj at obj resrcset S resrcset ct ct op get_current_access StateMonad Set Flow fn S State gt S atset S op put current access inatset Set Flow StateMonad fn S State gt atset inatset resrcset S resrcset op read op Subject ResourceExt gt StateMonad op write op Subject
57. blk in theMember idset Return the block id of a given resource op RB ResourceExt BlockId def RB res res blkid Figure 76 Definition of Block and related operations b Flow Next the notion of a flow is introduced in Figure 77 after declaring the various types of resources and blocks A flow is declared as a tuple of Subject ResourceExt and FlowModeSet Only two modes of flow ModeOfFlow Read and Write wil be considered in our simplified model ignoring a possible execute mode presented in the paper 12 The FlowModeSet attribute specifies the modes of flow under consideration from the source which is a Subject to the destination which is a ResourceExt Since it is represented as a set it is not required to define a NULL type and 64 a RW read write type as what DeCloss has done in his model An empty FlowModeSet will indicate no flow and a set containing both Read and Write modes of flow will be equivalent to the RW representation in DeCloss s model Our description does not exclude the possibility that the destination is another Subject A Transform is a collection of Flow tuples Each operation as used in the paper is associated with a Transform object which represents the resultant flows of an invocation The function MM represents all the flows between pairs of resources which will be actualized by the system operations It is declared in our model as a set of Transforms as it is the cumulative collectio
58. cessTuple transition at Terminate S 2 lt S proof Isa apply case tac at NV in S apply auto simp add BLP return def BLP monadBind def BLP currently accessible p def Let def BLP removeAccess def end proof theorem transition MakeKnown secure is fa S State S State at AccessTuple access secure at gt transition at MakeKnown S 2 S at proof Isa apply case tac at NV notin S VN and BLP access secure p at apply auto simp add BLP return def BLP monadBind def BLP currently accessible p def Let def BLP addAccess def end proof theorem transition MakeKnown not secure is fa S State S State at AccessTuple access secure at gt transition at MakeKnown S 2 S proof Isa apply case tac at _notin S NV and BLP access secure p at apply auto simp add BLP return def BLP monadBind def BLP currently accessible p def Let def BLP addAccess def end proof 107 theorem transition_state_secure is fa S State input Input securestate S gt securestate transition input S 2 proof Isa proof cases input show _Anda b _lbrakkBLP__securestate_p S input a b _rbrakk _Longrightarrow BLP__securestate_p snd BLP__transition input S proof fix ab assume al BLP__securestate_p S assume a2 input a b show BLP securestate p snd BLP__transition input S proof cases b case Terminate have snd BLP__transition a Terminate S _subset
59. ch Figure 52 shows an example of theorem pc_ok definition using simp add command The pcProperty predicate is converted to to pcProperty_p_def where is converted to p and _def is added to all op during the translation by Specware theorem pc ok is fa n Nat pcProperty evaluate n proof Isa simp apply induct tac n apply auto simp add Let def pcProperty p def evaluate def end proof Figure 52 Example of theorem pc ok using simp add command If we want to translate the Specware specification to the Isabelle specification the maximum number of elements allowed in any tuple type product is five Specware has added this restriction by design since by having too many elements in the tuple the specification may become unreadable Kestrel recommended the use of a record type instead of the tuple This is one of a few undocumented facts about the Specware to Isabelle Interface that the team encountered and valuable time was spent in troubleshooting just to isolate the problem It was particularly painful that no error was generated during the translation process Problems may be faced in proving of the translated Isabelle specification if we ee 99 were to use or to increase or decrease a natural number The correct way is to use a built in function in Metaslang like succ or pred for the increment or decrement of a natural number The use of the case of construct in a Specware specification
60. ch a given blockid filterBlock blockset BSet blkId BlockId BSet blockset fn i gt blockMatchBlockId i blkId oe oo Oo O oe oe Retrieve the block from a given block set that match a given blockid op getBlock blockset BSet blkId BlockId ReSet let bset filterBlock blockset blkId in if single bset then theMember bset else empty oe oe oo 6 Return the ID of a given block op getBlockId Block gt BlockIid def getBlockId blk let idset map fn i gt i blkid blk in theMember idset Return the block id of a given resource 113 op RB ResourceExt gt BlockId def RB res res blkid AIO RR AERA RIK IER RR ACK IRR RR AE ICR RK IEEE REOR ERB IRS IER AER KR LORS FORK Axioms describing property of Block RB Check is based on the policy matrix specified KRIEK KEREK RRR RRR AIR OK DIURCKOKUK CIO AK RR KERR IK KER IK KERERE KEE KER REI KI BRR AKER IE Y all Block types are nonempty axiom BlockNotEmpty is fa blk Block nonEmpty blk oo All of the resources of a given Block type have the same blkId axiom BlockResourceSameBlockId is fa blk Block resrcl ResourceExt resrc2 ResourceExt resrcl in blk amp amp resrc2 in blk gt resrcl blkid resrc2 blkid oe returns true if all blocks in a given BSet are distinct and do not overlap op distinctSets bset BSet Boolean fa bl Block b2 Block bl in bset
61. cs The first is types which describe collections of values The second component is operations which are functions on these values The last constituent is axioms and definitions which define the actions and properties of types and operations In the design of specifications a combination of top down and bottom up approaches may be employed The problem domain may be broken down into small manageable parts Each part is specified separately allowing one to focus on small individual parts of the problem A spec can be extended by importing other specs which essentially copies the imported spec into the target spec creating a larger and more complex spec Specs are also the objects used in morphisms which define the part of or is a relationship between two specs Morphisms allow for refinement of specs and provide the utility to take simple abstract specifications and refine them to more concrete complex specifications 14 The general form of a spec definition is shown in Figure 1 TrafficSpec spec body endspec Figure 1 Spec Definition b Types A type is a syntactic entity that denotes a set of values Types are collections or sets of objects and expressions that characterize those objects Specware provides several inbuilt types in its libraries These are imported automatically for every spec processed by Specware Users can declare new types or build or constitute new types from existing ones examples of which are
62. d in BB bb b a 5 a gt b caused by b op PO blkset BSet bb BBMatrix Boolean fa i Block j Block k Block i in blkset amp amp j in blkset amp amp k in blkset gt Refective Property direct flow to bb getBlockId i getBlockId i oo m Antisymmetric o direct flow to bb getBlockId i getBlockId j amp amp direct flow to bb getBlockId j getBlockId i gt 1 J amp amp Transitive o9 direct flow to bb getBlockId i getBlockId j amp amp direct flow to bb getBlockId j getBlockId k gt direct flow to bb getBlockId i getBlockId k Figure 91 Definition of Partial Ordering 78 The Partial Ordering is employed in the subsequent specification of Trusted Paired Ordering for the system The notion of a trusted subject defined at the beginning of this specification example is used here A trusted subject has been defined as one that is trusted not to downgrade information other what is intended for downgrading Given a partial ordering for B called Bbase a trusted partial ordering for the system is defined as in Figure 93 Bcontra is a subset of BB containing flows in contradiction to those identified in Bbase The operation derivebbflowset in Figure 92 derives the set of flows from the BBRecords inside the BBMatrix This is needed for comparison with the systemflows set oe oe BBMatrix contains a set o
63. deftbllloD uisuse e oot oseae iib es teat i hoi tessuto rt ed inde 40 Op assrenz func dehinttlon a e cot e D ERREXUE HR TUE ERES VUE AMT PUER dR CS 40 op get var_value definition aa usc Uoecod eor o t OBS secet re IRR EE ede Rd 41 Sample op initial _state definition 2e ooo oot e quttetotpa bbs tend test sp upQu aeons 4 Partial op transition definition ient esatto sione ie esa rea ee Pee te vien 42 OD property Get OM 6e Lope Pose tsei e usn dile buen 43 op evaluate dolre o o esM e Tad e AGERE A ud 43 theorem system_secure CET OM yaya 5 seed nio ordo RESI io eM listens 44 op pcProperty and theorem pc ok definition see 44 Example of theorem pc ok using simp add command 45 Ilustrated use of Type product o ausos eet eed cete afe ide ee ase e Pati e eer 47 Ilustrated use of Type record cx oem ee ooo e re ee tutta estere aut 47 Importing Specifications from General Library esses 50 Security Label Access Mode and Resource type Declarations 50 Declaration of Access Tuple and Transform Type eee 51 Declaration of Input Type ise reete tinere pinnae Peers teer e Uo Rene 51 Declaration of State Related Types State Monad and associated functions 51 Definition of dominates operation essere enne 52 Definition of security predicates to check security property 53 Definition of
64. domain model and implementation modeling language reference manual Computer Science Department Naval Postgraduate School Monterey CA http cisr nps edu downloads sdm DMRefManual_v2 pdf May 2008 Specware 4 2 Language Manual http www specware org documentation 4 2 language manual SpecwareLanguageManual pdf November 3 2008 124 10 INITIAL DISTRIBUTION LIST Defense Technical Information Center Ft Belvoir Virginia Dudley Knox Library Naval Postgraduate School Monterey California Professor Yeo Tat Soon Director Temasek Defence Systems Institute National University of Singapore Singapore Tan Lai Poh Ms Assistant Manager Temasek Defence Systems Institute National University of Singapore Singapore Dr Mikhail Auguston Naval Postgraduate School Monterey California Timothy E Levin Naval Postgraduate School Monterey California Dr Cordell Green Kestrel Institute Palo Alto California Dr Alessandro Coglio Kestrel Institute Palo Alto California Dr Stephen Westfold Kestrel Institute Palo Alto California Chuan Lian Koh Naval Postgraduate School Monterey California 125 11 Eng Siong Ng Naval Postgraduate School Monterey California 126
65. e sets could not be converted to code using the code generation functionality of Specware Research can be conducted to understand the process of code generation and generate an executable code from a verified model 4 Running Specware Isabelle on Alternative Platforms Running Specware and Isabelle on alternative platforms like MacOS and Windows may be further explored as it will eliminate our current dependancy on Fedora 89 THIS PAGE INTENTIONALLY LEFT BLANK 90 APPENDIX A GCD EXAMPLE A HASKELL EXAMPLE 19 A short example shows how the StateTrans Monad let you code in a fairly imperative style We will implement a variation on Euclid s algorithm for finding the greatest common divisor GCD of two positive integers as shown in Figure 96 while x do if x y then Yo else r up Im M y x x y return x Figure 96 Euclid s Algorithm for calculating GCD First we must define a type to represent the state as in Figure 97 type ImpState Int Int Figure 97 Declaration of State Next we define some simple state transformers Figure 98 to access and change the state We use the type and its sole value when a state transformer does not return a useful value getX getY StateTrans ImpState Int getX ST N x y x y x gety ST N x y x y y putX putY Int gt StateTrans ImpState putX x ST N x y 2 x y O0 putY y ST N x y
66. e 73 and is specified by the property propertyRB axiom in Figure 74 60 Block 1 Block 2 Block 3 Block n Exported Resource Set Figure 72 Blocks of Resources Internal Resource Resource Set Figure 73 The Resource Set 61 o All of the resources of a given Block type have the same blkId axiom BlockResourceSameBlockId is fa blk Block resrcl ResourceExt resrc2 ResourceExt resrcl in blk amp amp resrc2 in blk gt resrcl blkid resrc2 blkid oe oo returns true if all blocks in a given BSet are distinct and do not overlap distinctSets bset BSet Boolean fa bl Block b2 Block bl in bset oe oo o amp amp b2 in bset amp amp bl N b2 empty b1 b2 oe oe System element axiom Union of the resources of all blocks equals the resource set No other resourc xists other than those is sys resources Blocks of sys resources are distinct oe oe oo oe oe oo axiom propertyRB is fa sys System NN sys blocks sys sysstate resrcset fn i gt exported i amp amp full sys sysstate resrcset amp amp distinctSets sys blocks Figure 74 Property of Block In our model a Resource object is defined as in Figure 75 by a unique Resource ID a block identifier BlockId that identifies the block the resource belongs to and the memory essentially a set of bits assigned to
67. e and complicated proofs In the context of the project a specification language and verification system developed by the Kestrel Development Corporation is used We attempt to build upon the work perivously performed by DeCloss and to evaluate the usability of the newer features of Specware the discharging of proof obligations directly to Isabelle for proving via the Specware Isabelle interface and the modeling of the Least Privileged Seperation Kernel using Monads and inbuilt Set base library in Specware B INFORMATION FLOW ANALYSIS 1 Bell and LaPadula BLP The concept of mandatory access controls was formalized by Bell and LaPadula in a model commonly bearing their name 10 Numerous variations of the model have since been published but only a very simplified version will be considered in the context of this paper for the building of a sample security model using Specware Mandatory access control policy is based on security labels attached to subjects and objects A label on a user and an object are called security clearance and a security classification respectively A user labeled secret can run the same program as a subject labeled secret or as a subject labeled unclassified assuming the program is labeled unclassed Even though both the subjects run the same program on behalf of the same user they obtain different privileges due to their security labels For the purpose of the example in this thesis only the notion of sub
68. e is high if stmt 2 WriteLow amp amp exists fn i gt i 1 stmt 3 amp amp 1 3 High s 1 then false else true oe oe else true proof Isa simp end proof Figure 48 op property definition The evaluate definition is a recursive function which initializes the system state and does a number of transitions depending on the input nature number Figure 49 shows the definition of evaluate This function will run n number of line of the program The function is of recursive nature where it will recursively oe oe oo oe call itself until n 0 and the systemstate will be iniitalize to the initial state subsequently transition will happen until the initial n value op evaluate Nat SystemState def evaluate n if n 0 then initial state else transition evaluate n 1 proof Isa simp end proof Figure 49 op evaluate definition The system secure theorem shown in Figure 50 verifies whether or not the program loaded through the initial state in InitSpec sw violates the BLP property defined by the property definition We are not able to complete the proving of this 43 theorem using Isabelle as it requires an in depth understanding of the intrinsic of the Isabelle theorem proofing process In its place we created a theorem shown in Figure 51 to illustrate the proving of a trivial theorem in Isabelle This theorem
69. e remove access removes all tuples and accessses associated with the subject and object specified which have been previously enabled from atset The operations read op and write op are invoked via ReadResourceExt and WriteResourceExt transaction type calls respectively only when the specified input Flow is enabled EUR DE eese oco oe oen one FOR ac e oe oio ngon ok oe e eo oie oko BR aee eae oec o ee oie e o BK Xo aie or RR KR RK aee State Monad Definition GONE ORE ON OIA CORTE ON EUN ON TARE ORI pO eoo oceano alea c ooo oc oe op ook age scr oco ako aea a aeo ok ok y type StateMonad a State gt a State op a return x a StateMonad a tnm Stet op a b monadBind ml StateMonad a f a StateMonad b StateMonad b fn st gt let y stl1 ml st in fy stl CREER OK NOR OR UE TER KK OK ARIE AER RAK KK OK KU OK OK OR E ON ON OR OR KE OE UK ON OK KC OR OK KER OO KON GR UE CON ORO ON OK UK Ue TK System state functions State Monads for accessing and changing the state variables KERRIER RRR RAE ARE KER SRK BRAK KREIS RRR RIE BIR OK OK OR KKK BARKER KEKE Y op get_access_by_at at Flow StateMonad Set Flow fn S State gt S atset fn i gt i subj at subj amp amp i obj at obj S 5 Access Functions to retrieve and set values inside states op currently accessible at Flow StateMonad Boolean curr lt get access by at at return single curr amp amp at fset lt theMember c
70. e version 4 2 5 Results and recommendations pertaining to the different areas of exploration are summarised below A SPECWARE MetaSlang in Specware is a rich language for specifying the security model but the available documentation is not sufficient for a beginner to achieve functional programming in particular more examples are needed To help beginners to smoothen the learning curve for Specware we recommend that the Specware Language manual 26 include more exhaustive examples of how each of the Mestaslang constructs can be used and that the tutorial documentation include more sample specifications in Specware Also documentation built in and examples for the new Set base library should be included The current version of Specware for Linux does the support the use of x symbols as x symbols have some conflicts with the version of XEmacs used X symbols are useful when writing the specification as they greatly enhance the readability of the specification Email support from the Kestrel Institute on Specware has been responsive but is currently provided by a single person at Kestrel A discussion group or forum would be extremely useful for one who is just learning the language It would promote a more proactive and interactive learning environment and provide a learning ground for beginners to learn from each other and to share their learning experiences B ISABELLE While SNARK is an automatic theorem prover Isabelle is an
71. ection was used for the purpose of discussion 1 Specware Model A walk through of the specification was first done with Dr Coglio Alessandro and Dr Stephen Westfold from Kestrel Improvements suggested are as follows Use of Type records in place of Type products Type records are essentially similar to type products except that the components called fields are identified by name instead of by position The ordering of the filed typers has no significance This makes the specification clearer and more readable An example to illustrate the use of both types is shown in Figure 53 and Figure 54 46 Definition using Type product type Resource ResourceName SecLabel Example op label Resourc SecLabel def label resrc resrc 2 Alternative way of representing def function def label name lab lab Figure 53 Illustrated use of Type product Definition using Type record op label Resourc SecLabel def label resrc resrc label type Resource name ResourceName label SecLabel Figure 54 Illustrated use of Type record 2 Use of Set instead of List The team has always pondered the lack of the support for Set in the Specware Inbuilt and Base Library It was only understood during the visit that the Set specification is not released and will only be available from Specware version 4 2 5 Set predicates are available fo
72. ed Unclassified UU NSN 7540 01 280 5500 Standard Form 298 Rev 2 89 Prescribed by ANSI Std 239 18 THIS PAGE INTENTIONALLY LEFT BLANK ii Approved for public release distribution is unlimited SECURITY MODELING AND CORRECTNESS PROOF USING SPECWARE AND ISABELLE Chuan Lian Koh Civilian Defence Science amp Technology Agency Singapore BEng Osaka University Japan 1996 MTech Institute of System Sciences National University of Singapore Singapore 2002 Eng Siong Ng Civilian ST Electronics Limited Singapore BSc Hon University of Portsmouth UK 2000 Submitted in partial fulfillment of the requirements for the degree of MASTER OF SCIENCE IN COMPUTER SCIENCE from the NAVAL POSTGRADUATE SCHOOL December 2008 Authors Chuan Lian Koh Eng Siong Ng Approved by Mikhail Auguston Thesis Co Advisor Timothy E Levin Thesis Co Advisor Peter J Denning Chairman Department of Computer Science ili THIS PAGE INTENTIONALLY LEFT BLANK iv ABSTRACT Security modeling is the foundation to formal verification which is a core requirement for high assurance systems This thesis explores how security models can be built in a simple and expressive manner using the Metaslang specification language in Specware The models are subsequently translated via the Specware to Isabelle Interface to be proven for correctness in Isabelle which is a generic interactive theorem proving environment It is found that the translation betw
73. ed as a tuple of color and the number of state changes 32 types Traffic_Light Color lt times gt int consts light_changes Color lt Rightarrow gt Color defs light_changes_def light_changes c lt equiv gt if c Red then Green else if c Green then Yellow else Red consts next_state Traffic_Light lt Rightarrow gt Traffic_Light defs next_state_def next_state x lt equiv gt light_changes fst x snd x 1 theorem run_traffic_Obligation_subsort lt lbrakk gt lt not gt n lt le gt 0 lt rbrakk gt lt Longrightarrow gt int n 1 lt ge gt 0 by auto consts run_traffic nat lt Rightarrow gt Traffic_Light recdef run_traffic measure size run traffic n if n lt le gt 0 then Yellow 0 else next state run traffic n 1 theorem light matches light changes fst x fst next state x apply simp add light changes def next state def done Figure 30 Translated Isabelle specification for the traffic light modeled as a tuple of color and the number of state changes 5 Discussion and Lessons Learned The state tuple provides a concise way of representing state and tracking changes The two representations are however observed to have similar effects and the List model is adopted in the subsequent Simple BLP property example to harness the inbuilt support of Specware for List for easy manipulation of its elements The traffic light model shows the
74. ed in sequence as they are used Isabelle unlike Specware does not tolerate the usage of types and operations which have not been defined at the point where they are used Secondly as a general guideline it is always good to decompose functions into smaller intermediate functions as doing so frequently makes proving more direct and easier Proofs of the sub parts can then be used to compose proofs of composing types Thirdly the Kestrel team cautioned the overuse of axioms as they may not be totally consistent with one another This retards rather than facilitates proving 4 Proving Using Isabelle The Kestrel team attempted the proving of the BLP specification using Isabelle The team observed that although the theorem looks trivial the proof requires extensive knowledge and experience in logical calculus and Isabelle Isabelle is a powerful interactive theorem prover but has a substantial learning curve The proof is done interactively on Isabelle and the result is copied back into the original Specware specification The final specification and the corresponding proof will be shown and discussed in the next section Overall it was a fruitful visit and a great learning experience The authors regret that the visit was not performed in an earlier stage of the research A lot more could be learned from the staff at Kestrel to supplement the inadequacies in the team s technical knowledge and skills and the lack of access to Specware exam
75. een Specware and Isabelle is almost seamless and there is much potential in the use of Isabelle HOL to discharge proof obligations that arise in developing Specware specifications although the actual proving requires substantial knowledge and experience in logical calculus THIS PAGE INTENTIONALLY LEFT BLANK vi II HI IV TABLE OF CONTENTS EN TROD CUTON cicsuoncesicsasevauecoacnaders eos checa cost eehasonscssbessoudcnsneieiasonecssbesseubscusansluseates 1 BACKGROUND ete tnpt p sovssvestesncstvaivanisnsotconss cussenasboatevoeosvensnebsdsonseonivenasbenssedeee 3 A FORMAL METHODS MODELS AND VERIFICATION 3 B INFORMATION FLOW ANALYSIS e esee ee eroe eee eoo etn sten sees e tae ena etas 6 1 Bell and LaPadula BLP cccccccscscscssscscscscscscscscccccccccccccccccccsoees 6 2 Least Privilege Separation Kernels LPSK 6 C SECURITY MODELING AND ANALYSIS cessere eere een ene en eene 7 OVERVIEW OF SPECWARE AND ISABELLE eee ee eee eee eene etn een etn sn use 9 A SPEC WARE DESCRIPTION ii ibescofe dye eseeceteatesadee esie cid ev onte bio eS co supe debes 9 B SPECWARE FUNCTIONALITY eee eee eoe e eoe en oe eo stans eee etae eaa etas en eoa 10 1 WAKA TASH DIA E OEE 10 a NY A AERA E E E A EET 10 b m EEEE EE EEEE 11 c Ops and Defsio ener e DRE retea raisa iiaia 12 d C
76. el that if a flow occurs for a system state it must be because the flow has been enabled in the access table in that particular state Consequently the concept of a SecureSystem is straightforward It is defined as a summation of these properties of Transaction and Flow 86 VI CONCLUSION A CONCLUSION In the course of this thesis work the team attempted to come to terms with Formal Methods FM tools starting from a minimal mathematical background and knowledge about these tools Given the state of FM tools today the learning curve is complex and intellectually steep but momentum picks up after negotiating the first few slopes The team was lucky to be exposed to both the model checking e g refutation as in Alloy Analyzer and theorem proving as in Specware and theorem prover like PVS and Isabelle to appreciate both types of FM The team s work however was very much limited to security modeling and code verification using Specware and Isabelle There is a great deal more to be learned in this area The main challenges encountered by the team include coping with the mathematics and proving logic and paradigm shift between imperative programming and functional programming the limited documentation and examples on Specware and the overwhelming load of documentation and details in Isabelle where we struggled to locate the logical starting point However as this was a team effort and even though we were far from being twice
77. eorems for secure state 71 g Partial Ordering and Trusted Partial Ordering Figure 91 shows our attempt to specify the Partial Ordering of the inter block flows defined by BB Partial Ordering is a relation defined on a set having the properties that each element is reflective the relation is transitive and if two elements are in relation to each other the two elements are equal antisymmetric The Partial Ordering of BB ensures that information is not allowed to flow circularly among the blocks in the relationship i e if information leaves a block there is no transitive flow that will lead the information back to the block direct flow to is defined as a helper function to restrict flow consideration to only those direct flows between the two blocks under consideration ok ORO BRO se eo AIR IR oec ae sock sede SALI eoe ox c olia ow sock HAIER ia e aepo av ov clo Oo ex Partial Ordering of BB Semantics to describe flows between blocks to be defined in such a way that information is not allowed to flow circularly i e if information leaves a block there is no transitive flow that will lead back to itself Important to note that any 2 blocks are not required to be related by a flow DRS I REI wee NIK aco e cock sean KER anode ac IR SIG A cavo oc argo sporco I IE Kok stipe AKI BK I egeo y op direct flow to bb BBMatrix a BlockId b BlockId Boolean Write in BB bb a b 5 a gt b caused by a Rea
78. eq S by rule tac BLP__transition_Terminate_subset_eq with b Terminate input a b have new_in_old snd BLP__transition input S _subseteq S by auto from al have S _subseteq BLP__access_secure_p by auto simp add BLP__securestate_p_def with new_in_old have snd BLP__transition input S _subseteq BLP__access_secure_p by rule subset_trans thus thesis by auto simp add BLP securestate p def next case MakeKnown show thesis proof cases BLP access secure p a case True thus thesis proof have new state snd BLP transition a MakeKnown S insert a S by rule tac BLP transition MakeKnown secure from al have S secure S NV subseteq BLP access secure p by auto simp add BLP securestate p def with new state a2 b MakeKnown BLP access secure p a show thesis by auto simp add BLP securestate p def mem def qed next case False thus thesis proof have new state snd BLP transition a MakeKnown S S by rule tac 108 BLP transition MakeKnown not secure with al have BLP securestate p snd BLP transition a MakeKnown S by auto with input a b b MakeKnown show thesis by auto qed qed qed qed qed end proof endspec 109 THIS PAGE INTENTIONALLY LEFT BLANK 110 APPENDIX D LPSK MODEL A LPSK SW LpskSpec qualifying spec import Library General ERE IRR RE RAO AIK ROR KEN RK RIE RRA KER ER KRAE LACK KR KERR REN KER RR KKK KI
79. er The version of Specware used for the project is 4 2 2 An unofficial release of Specware version 4 2 5 was also used in the later stage of the project which supports Set and has additional support for Monads B SPECWARE FUNCTIONALITY 1 MetaSlang MetaSlang based on higher order logic is the specification and programming language used in Specware The Specware Language Manual contains a description and extended BNF of the grammar of the Metaslang language An extracted portion of the core grammar is shown here but it is not intended to be comprehensive The reader is recommended to refer to the Specware documentation for a more complete explanation MetaSlang is essentially a functional language It includes syntactic constituents for describing functional semantics within a specification as well as constructs for describing composition refinement code generation and proof capabilities Specification constituents include types expressions and axioms which can be used to describe domain specific formalisms 14 The MetaSlang grammar follows a functional style of programming which is valuable for proving properties regarding functions a Specs A specification is a finite presentation of a theory in higher order logic 17 Specifications or specs provide the means to describe abstract concepts of the 10 problem domain which is the first step in building an application There are three major constituents of spe
80. eration for top level invocation is defined as shown in Figure 105 This allows us to furnish an initial state and applies it recursively to obtain the result The greatestCommonDivisor further encapsulates the applyST by furnishing the initial state in terms of its individual components oe oo Encapsulating operation invoked with initial state op applyST StateMonad Nat gt GCDState gt Nat GCDState def applyST fnsm initstate fnsm initstate oo oe Top level Encapsulating operation with 2 input numbers to 5 calculate gcd on op greatestCommonDivisor Nat Nat gt Nat def greatestCommonDivisor x y applyST gcdST x y 1 Figure 105 Encapsulating Function and Initialization 94 APPENDIX B BLP PROPERTY MODEL A TYPEDEFSPEC SW oe This specification contains all the type declaration required by the BLP property specification oe TypeDef spec Initial type declaration type Name String type Value Integer type Index Nat type ProgCounter Nat type Label High Low 9 Variable declaration type Variable Name Value Label type Variables List Variable 6 Input declaration type Input List Value Index oe oe Statement declaration 6 assignl variable name variable name gab 6 assign2 variable name value eg a 5 type TypeOfStmt ReadLow ReadHigh WriteLow WriteHigh Assignl Assign2 Ifthenl
81. es and a set of resources RSet as in Figure 85 As already mentioned State represents the components of the system that can change An access tuple represents a request to the kernel for access to a system resource It is expressed in the form of a Flow object The kernel arbitrates every access attempt and determines if an access is allowed based on the transaction type 47TTransaction defined in Figure 85 and the policy of the system Four transaction types have been defined for the model Each transaction potentially causes some change in the system state ReadExternal and WriteExternal in particular may result in a flow in the system The read op and write op are abstract operations but they invoke flows which result in changes in the subject and accessed object s memories respectively Changes in the memory of subject and object memories are captured in the resrcset component of the State 70 type ATTransaction MakeKnown Terminate ReadResourceExt WriteResourceExt Figure 85 Different types defined in ATTTransaction d State Monads The State Monad is declared as in the previous model for BLP Additional State Monads are defined in Figure 86 to access and change the state variables namely atset and resrcset The function currently accessible checks to see if a particular access has already been granted by the system through a prior MakeKnown transaction type call add access adds and enables an access atset whil
82. esult is in that other monadic type The binding operation contains the logic essential to execute the monadic functions or registered callbacks In Specware this function is named monadBind The explanation here is far from complete and will be left as an exercise for users to learn more about Monads We will leave with some simple explanation of the declaration of the Monad shown in Figure 6 which is used in most of our models The type constructor is defined by the first declaration of StateMond a where StateMonad represents the name of the Monad and a is the underlying type The unit or return function is represented in the next statement and it essentially maps a value of type a to StateMonad a Lastly monadBind defines the binding operation and is used implicitly rather than explicitly in many Monadic operations in this thesis op op type StateMonad a State gt a State StateMonad b a return x a StateMonad a fn st gt x st a b monadBind m1 StateMonad a f a gt StateMonad b fn st gt let y stl ml st in f y stl Figure 6 State Monard and accompanying monadic functions The Haskell programming language is a functional language that makes heavy use of Monads The concept of a Monad is not intuitive and is hard to grasp for most beginners It will not be possible to go into great detail here and readers are advised to find out more from the many tutorials avai
83. exported i in let exres sys sysstate resrcset N fn i gt exported i in intres M exres sys sysstate resrcset amp amp intres N exres empty RIERA KARA KERR RR RK LIRIK DK HAC RON OR TORO OK KK ce LA I OK KK OC RAR RB RRR RNC LER IE RRR 112 Memory Related Axioms FOR ERR LORIE RK RRL AIK RRR AIR LTR ARE ICIS KI SK EEA E RE BKK RRL RRR BORIS REY axiom propertyResourceMemoryDistinct is fa resrcl Resource resrc2 Resource resrcl rscmem resrc2 rscmem empty resrcl resrc2 PRE BR ROR EIR IER KEN RK IR ROKR A RR FERRIER RICK RIE RR ROK HOR Ke RR OK CONCI RRA KER AR State Monad Definition ERR RAE ARK KAA AREER RE AIR NK OK CK KIKI HAE AER LEI RAAB RELI REESE ERY type StateMonad a State gt a State op a return x a StateMonad a fn st gt x st op a b monadBind ml StateMonad a f a gt StateMonad b StateMonad b fn st gt let y st1 ml st in fy stl EREKE RARER ARR GUN AIAG RR LORRI IR RRR AI AER KK ORE UNO ORONON ROR ARES CORO RRR se esee eaae Block Manpulation Operations Needed for linking resource to the block it belongs to amp vice versa WOKCKURCKOK RRR EKRE RERAN EREEREER Te RARE RIKEN ARR KKK E EREEREER EERE KERRE BIN deo oe es op blockMatchBlockId Block BlockId gt Boolean def blockMatchBlockId blk blkId fa resrc ResourceExt resrc in blk gt resrc blkid blkId oe oo Retrieving the blocks of given block set that mat
84. f BBRecord record block block flowset We would like to extract out the allowed flows from this bearing in mind that a flow is a tuple consisting of a subject object fmode op derivebbflowset bbm BBMatrix Set Flow let setsetflow map bb2flowset bbm in setsetflow oe oe oe oe oe oe op bb2flowset bb BBRecord Set Flow let blsubject bb b1 N fn i gt active i in let b20bject bb b2 in let bbduple blsubject b2object in map fn a b gt subj a obj b fset bb fset bbduple Figure 92 Definition of op to extract flows from BB Matrix RARER RAR AAR RAR OK ene oo OR GE Oi Wo ov eoe ORC oe e Eo OK KK OK OR BND KERR ERR RAK AKI KIRK KK ene Trusted Partial Ordering of BB Bbase Trusted partial ordering for system Trusted Subject is a Subject that has undergone rigorous analysis amp is trusted not to downgrade information other than the information it is intended to downgrade He is allowed but not required to violate the partial ordering Flows will exist in the System that will violate the partial ordering bcontra RE RRR Ope eoo oec AKER week oae aeos se kc e ole ale oae aie ec eoe RII e ac oie ok oe eoe e AKER KARR KR RER ese caes theorem TPO is fa sys System bbase BBMatrix ex blkset BSet bcontra Set BBRecord 79 bcontra BBRecord and RB rs oec oo oo oo oe oe oe oo oe oe System Transform flows will be t
85. fication and proven in Isabelle 1 Color Definition There are three colors in a traffic light namely red yellow and green The trivial example described here models simply how the color changes in a traffic light system Figure 19 shows a definition of type color in Specware while Figure 20 shows the Isabelle specification translated from the Specware specification 26 Define that color can be Red Yellow or Green type Color Red Yellow Green Figure 19 Type Color definition in Specware Red datatype Color Green Yellow Figure 20 Type Color definition in Isabelle 2 Op light_changes Light changes is defined as an op that transits the current color to the next color Figure 21 shows how the op light changes is defined in Specware while Figure 22 shows the translated specification in Isabelle Define light_changes function The function will return the next color based on the inputed color op light_changes Color gt Color def light_changes c if c Red then Green else if c Green then Yellow else Red A oe oe oe oe oe Figure 21 Light changes definition in Specware consts light changes Color lt Rightarrow gt Color defs light changes def light changes c lt equiv gt if c Red then Green else if c Green then Yellow else Red Figure 22 Light changes definition in Isabelle 3 Traffic Light as a List of Colors
86. iOn ssscscvasjsccessnadentscccdeacasdescesoundecees ie nan Vo eruere sS ed vh 92 Declaration ot GE DS tate aceite ona taie i taltete aa beide 93 Declaration of Monads and Monadic Function eee 93 X and Y Manipulators senenin AUSTIN ER Eee e Ape Era aiaa 93 State Transition Function gcdST cierre rhe denne eaae eee eto ER eo as eee einn 94 Encapsulating Function and Initialization eene 94 xiii THIS PAGE INTENTIONALLY LEFT BLANK xiv Table 1 Table 2 Table 3 LIST OF TABLES Common XEmacs and Specware commands List of Tasks for Specware 4 2 2 to run in Fedora 8 Transaction types supported in model XV THIS PAGE INTENTIONALLY LEFT BLANK xvi ACKNOWLEDGMENTS We would like to express thanks to many individuals who have influenced and assisted us during the development of this thesis Thanks to our thesis advisors Prof Mikhail Auguston and Prof Timothy E Levin for their valuable advice and guidance We believe that the knowledge they have imparted to us will benefit us in our future endeavors Thanks to Dr Cordell Green Dr Alessandro Coglio and Dr Stephen Westfold from the Kestrel Institute for their support with Specware Thanks to Prof George Dinolt for providing us with valuable advice and insight to a theorem prover like Isabelle Thanks to CDR Alan Shaffer for sharing with us on his experience in building a security
87. in the next state also being secure Also an actualization of a flow in the system due to a read or write operation for a particular system state implies that the flow is enabled for that system state From the two theorems we would also be able to deduce that starting from an empty secure state all subsequent states should be secure based on the properties defined in SecureSystem op secure write transition S1 State at Flow Boolean if Write in at fset then let S write op at subj at obj S1 2 in get resource memory at obj S1 1 get resource memory at obj S 1 gt currently accessible at S1 1 else false op secure read transition S1 State at Flow Boolean if Read in at fset then let S read op at subj at obj S1 2 in get resource memory at subj S1 1 get resource memory at subj S 1 gt currently accessible at S1 1 else false op securestate S State policy Policy Boolean fa at Flow at in S atset gt access secure policy srm policy bbm at theorem EmptySecure is fa sys System sys sysstate atset empty amp amp securestate sys sysstate sys pol theorem SecureSystem is fa S State input Input sys System securestate S sys pol gt securestate transition input sys S 2 sys pol amp amp secure write transition S input at amp amp secure read transition S input at Figure 90 Security Th
88. ion of Resource Sets 59 The set of ResourceExt elements is partitioned into blocks which also constitute equivalence classes Every ResourceExt element in the specification is assigned exactly one and only one Block element Subjects and other exported resources are allocated to blocks by the separation kernel Conversely each block defined must have at least a resource allocated to it as an empty block would not be useful This is described by the axiom BlockNotEmpty in Figure 71 BSet is declared to be the set of all blocks defined for a particular system oo Partitioning of resources into blocks type Block Set ResourceExt 6 set of blocks type BSet Set Block oe Each block must have at least one resource allocated to it since an empty block is useless and invalid axiom BlockNotEmpty is fa blk Block nonEmpty blk Figure 71 Declaration of Block and BSet A Block is defined to be a set of exported Resources as shown in Figure 72 All the resources inside a Block have the same Blockld as described by the axiom BlockResourceSameBlockld All Blocks in a system are distinct sets which do not overlap Any ResourceExt in the system must reside within a Block Consequently the summation of all Resources inside all defined B ocks should equal that of the entire exported resource set considering that no ResourceExt is defined outside a Block This is shown pictorially in Figure 72 and Figur
89. is evaluate whether the input program is secure theorem system secure is fa n Nat property evaluate n This proof could not be complete in Isabelle It require an more in depth understanding of Isabelle proof Isa simp apply induct tac n apply auto simp add Let def end proof oe oe oe oe oe Figure 50 theorem system secure definition oe This function checks whether the program counter is greater than 0 op pcProperty SystemState Boolean def pcProperty s if length s 4 1 0 then true else false proof Isa simp end proof oe 6 This trivial theorem will confirm that Prog counter will remain greater than 0 theorem pc ok is fa n Nat pcProperty evaluate n proof Isa simp apply induct tac n apply auto simp add Let def end proof Figure 51 op pcProperty and theorem pc ok definition 3 Discussion and Lessons Learned Many valuable lessons on the use of Specware and Isabelle were learned in the process of building this model We learned that instead of using the simp add command in Isabelle we can add proof Isa simp end proof at the end of each op definition This 44 will instruct Isabelle to add the op definition after it is being proved to the list of simplification rules which can be used for proofing of other op definition or theorem All the codes listed in Figure 39 through Figure 51 used this proof Isa simp end proof approa
90. ject and object will be considered Mandatory access BLP rules can be expressed as follows with SecLabel representing the security label of the indicated subject or object Simple security property Subject s can read object o only if SecLabel s dominates SecLabel o property Subject s can write object o only if SecLabel o dominates SecLabel s 2 Least Privilege Separation Kernels LPSK The separation kernels concept was introduced in 1981 by Rushby 11 A separation kernel divides all the resources into blocks sometimes called partitions The actions of an active resource in one block are isolated from another active resource in another block unless a communication is explicitly defined 12 The common application of the separation kernels concept includes Virtual Machine Monitors VMM process isolation enforcing avionic related policies and security policies 12 A separation kernel where resources are allocated to blocks in a fixed manner is called a static separation kernel and is desirable for simplicity of design 3 The Principle of Least Privilege 13 is fulfilled by granting only the least set of privilege to an active resource in LPSK Part of this thesis attempts to implement a security model based on A Least Privilege Model for Statics Separation Kernels 12 published by The Center for Information Systems Security Studies and Research CISR at the Naval Postgraduate School NPS C SEC
91. l to guide the proof interactively to completion The team began the exploration of Monads at this point as an alternative representation of the state changes as it is suspected that the construct of the state changes as is currently used in the BLP property model may be overly complex making proving on Isabelle non trivial A simple Specware example was created based on a widely available Haskell example as in Appendix A to explore the support and use of Monads on Specware 25 i Haskell Monad I I I Example Traffic Light Model BLP property Model BLP Model N c oe e om o Simple Monad Example Refinement Proving using Isabelle LPSK Model Figure 18 Modeling Approach As a natural next step the BLP model and the Simple Monad example were merged to obtain our first security model specification BLP Model with Monad using Specware This model was used for the discussion and refined during the team s visit to Kestrel The Kestrel team attempted a proof of the specification using Isabelle which is documented in more detail later in a later section After the visit the BLP Model was used as a base specification for a Least Privilege Separation Kernel LPSK B SIMPLE TRAFFIC LIGHT MODEL Before specifying the security model the team explored representing traffic light state changes in Specware This Specware specification is subsequently translated into an Isabelle speci
92. l undo all the proof steps and return to the beginning of the Specification The Undo command will undo the current statement The Next command will execute the current statement The Use command will execute all the statements till the end of the specification and the Goto command will execute up to the current statement Figure 26 shows an example of a 29 counterexample found before axioms are being applied After the axioms are applied in the proof Isabelle was only left with one subgoal to prove as shown in Figure 27 Figure 28 shows the end result of the proof of the theorem File Edit View Cmds Tools Options Buffers A A Options Proof General Isabelle ListSpec TrafficListSp Scratch thy This is a simple Specware specification that modelled a traffic light state changing process using list TrafficListSpec spec Define that color can be Red Yellow or Green type Color Red Yellow Green Figure 25 Screenshot of Isabelle command menu proof prove step 0 qoal 1 subgoal TM 7 y lt int length a ak gt light changes x nat y x nat y 1 Counterexample found x Red Red y 0 else crum i re simp EDEN lt lbrakk gt y ge 0 y lt int length x 1 lt rbrakk gt lt Longrightarrow gt light changes x nat y x nat y 1 using al a2 M apply auto M done endi Figure 26 A counter example is found by Isabelle before using the two
93. lable on the web 18 19 15 The Specware User Manual contains only a very brief description of Monads Section 2 6 16 without furnishing any concrete example on their usage We translated a simple Haskell 19 example to Specware to better understand the concept and its support in Specware Both the Haskell specification and the corresponding Specware one can be found in Appendix A 2 Specware to Isabelle Translation The specification in Specware can be translated to Isabelle Specification using the command Ctrl C TAB in the Specware to Isabelle Interface A Specware definition may translate into one of three different kinds of Isabelle definitions defs recdefs and primrecs primitive recursions Simple recursion on coproduct constructors translates to primrec but if the function has multiple arguments only if the function is curried Other recursion translates to recdef which in general requires a user supplied measure function to prove termination Non recursive functions are translated to defs except in some cases they are translated to recdefs_ which allow more pattern matching 20 Figure 7 shows a sample Specware specification while Figure 8 shows the Isabelle specification translated from the sample Specware specification op transition State gt State def transition s succ s 1 succ s 2 proof Isa simp end proof op evaluate Nat gt State def evaluate n if n 0 then 1 0 else transition eval
94. laims Axioms Conjectures and Theorems 13 e Set AIG List ir IW ERES FOR SEEK PER A iesit 14 f IVI ON GAS e eer ODE QUE TR HD Ud a eaa DR en Aeg 14 2 Specware to Isabelle Translation esee eere ee eere ee eenue 16 3 Basic Specware Operation sssesssesssecssocesocesoocesoeesooecsscessocesoosesoseose 17 C ISABELLE PROVING APPROACHES eere ee ee ette eee en neenon oetnoes 18 1 Apply style PEOO S eee eee esto eor n eon voa soseeyseenesevsscsvevensssuesevesntene 18 a AD DIVAN O eoa Cad pa IER OUR RN Ven dc d a 18 b AD DIV UTILES BM 111 H6 o RR E TT CETT 19 c apply stip add x1 x2 ie ettet tette erano ea aret h E 19 2 Structured Isar Proofs scsissccissyssoicesseacebicescenesessucbeduescensatuessoboenesonsadevy 19 D SETUP OF DEVELOPMENT ENVIRONMENT IN FEDORA S 20 1 XEmacs Version 21 5 28 5 ccccrscccrsssrsercscoesccsssscocssnecseesssssscossenecse 20 2 Isabelle 2008 Version 2 oer epeore sebo tb eiua ense rev s cop eek eek pne ae SE PP EP ERE E 21 3 Specwar Version 4 2 2 areec testes eeskVudnev ev be eae n epe HERR UNE RO Ec EP PEU US 21 SECURITY MODEL ceteri loop echas MM P n D eta Mie E 25 A MODELING STRATEGY i ooteiipe sect sa eee eee redeo sorte etn eco b oedeve niece 25 B SIMPLE TRAFFIC LIGHT MODEL seen ueneno eene eo etn enne tnos tnaeo 26 1 Color Definifiob init ooo tese bete buio ma xo Erebi pe Pa
95. lation The resultant implementation consequently looks cumbersome as only the onlyMember operation was available at the team s disposal to retrieve a member from a set which is a Singleton Although axioms could be and have been defined to ensure that such sets are Singleton we are still left with the ugly if then else construct in the functions as onlyMember could also be invoked on a set which is a Singleton 63 REAR REAR EK AAR ERR RAK RRA KERR LAK ERK BR RRR KISEKI RE OR KORORUR KCOKCIEOAE Block Manpulation Operations Needed for linking resource to the block it belongs to amp vice versa ERRER AK RIKARE KLE RR KK KAR KERR KR LER ERR RRR ERE RRR BRAKE RRR RK CUR RUKOR CK KEREK KKK Y op blockMatchBlockId Block BlockId gt Boolean def blockMatchBlockId blk blkId fa resrc ResourceExt resrc in blk gt resrc blkid blkId oo oe Retrieving the blocks of given block set that match a given blockid filterBlock blockset BSet blkId BlockId BSet blockset fn i gt blockMatchBlockId i blkId oe oo o oo oe Retrieve the block from a given block set that match a given blockid getBlock blockset BSet blkId BlockId RSet let bset filterBlock blockset blkId in if single bset then theMember bset else empty oe oo o 5 Return the ID of a given block op getBlockId Block gt BlockId def getBlockId blk let idset map fn i gt i blkid
96. le Assignl X Y statement else if stmt 2 Assignl then oo assign RHS to variable specified by LHS let new mem assignl func stmt 3 stmt 4 vars inputLow inputHigh in Update prog stat increment the program counter let new prog prog 1 stmt 5 1 in new mem 1 new mem 2 new mem 3 new prog 6 Handle Assign2 X 5 statement else if stmt 2 Assign2 then assign RHS to variable specified by LHS let new mem assign2 func stmt 3 stmt 4 vars inputLow inputHigh in 5 Update prog stat increment the program counter let new prog prog 1 stmt 5 1 in new mem 1 new mem 2 new mem 3 new prog The Ifthenl statement was not used it can be extended in future else if stmt 2 Ifthenl then handle if then else statement let exprval cond eval stmt 3 stmt 4 GE s 1 s 2 S43 5n 101 let next_stmt if exprval then stmt 5 1 else stmt 5 2 in let new prog prog 1 next stmt in vars inputLow inputHigh new prog 5 Handle stop statement else if stmt 2 Stop then return the current state oo el oe 5 u by default return the current state for unknown statement S by defualt return the current state for unknown statement se s with simp this def will be added into the list of simplication rule for future proofing proof Isa simp end proof oe 0 ra check the system state for writing high to low BLP property op property
97. le interface It is recognized that it is still work in progress and rare instances exist where the convertor may turn out Isabelle syntax which is not accepted by Isabelle The team has reported a few such encounters to Kestrel and many such as the one involing the use of case of construct have been resolved in Specware version 4 2 5 A number of these may not be implementation bugs but rather design and implementation decisions by Kestrel but were undocumented When the problems are encountered with proving in Isabelle first the cause of the problem must be determined e g whether it is caused by an inadequacy in the translation tool or that the proof demands more input from the user This is a time consuming process for users with limited knowledge about the intrinsics in the translation and the syntax of the Isabelle language 84 D SETTING UP OF SPECWARE ISABELLE DEVELOPMENT ENVIRONMENT Specware and Isabelle together with the Specware Isabelle Interface currently are not supported on Windows The development environment for the project was set up on a Fedora 8 platform running as a VMWare virtual machine on a Windows Vista machine Glitches were encountered during the setup and valuable time was spent getting the software to work To make the process as painless as possible for new users we have furnished detailed documentation on the setup process in this report The setup was done using Specware 4 2 2 and Isabelle 2008 ver
98. ll read in the next statement oo oe perform it and then call next op transition Input StateMonad Boolean def transition at input transaction case input transaction of MakeKnown gt curr currently accessed at if curr amp amp access secure at then addAccess at return true else return false Terminate gt curr currently accessed at if curr then removeAccess at return true else return false op evalProgram InputList StateMonad List Boolean def evalProgram inputs case inputs of gt return inp r inputs gt rl transition inp res evalProgram r inputs return rl res Figure 63 State Transition h Theorems Simply put the theorem in Figure 64 just means that the empty state is secure Empty state refers to the state where the current access is empty i e the state where the system has not handed out any descriptors for access to the resources 54 oe theorem stating that an empty Current Access Matrix is a secure state theorem EmptySecure is securestate empty oe Figure 64 Theorem Empty is Secure Two supportive theorems Figure 65 have been added to facilitate the eventual proving by Isabelle One states that if the current attempted access is secure it will be added to the set of access tuples which make up the Current Access It should be noted that this hold
99. lue from low input and updates the read value into the specified variable together with a Low label indicating that the value is from low input Figure 42 shows the definition of read low func 5 function to read from low input and assign to variable specified by LHP op read low func LHP MemoryState MemoryState def read low func var name mem state let read value read low mem state 2 in update variable var name read value Low mem state proof Isa simp end proof Figure 42 op read low func definition The read high func definition is similar to the read low func except that it is reading from high input and hence the label is High The assign1 func definition uses the case method to extract the variable name from RHP as shown in Figure 43 and calls find variable in MemorySpec sw to get 39 the variable tuple stated by the RHP If the variable is in the variable list the keyword Some can be used to retrieve the tuple and update the variable using update_variable in MemorySpec sw None indicates that the variable was not found and the definition will just return the current memory state 5 function to assign a value of a variable to a variable LHP op assignl func LHP RHP MemoryState gt MemoryState def assignl func l r mem state find out the value of the variable specified by RHP then assign the value to LHP if not variable not found just do nothing case r of
100. ment type declaration 36 A Statement is being declared as a tuple as shown in Figure 37 Initially the team intended to represent the statement with six elements but the Specware translator only allowed the maximum of five elements in a tuple Therefore we created an extra tuple called NextProgCounter in Stmt The first ProgCounter indicates the index of the next statement to execute and the second ProgCounter is reserved for future implementation of if then else statements Sample code on how if then else statements can be included in the model is available as part of Appendix B 5 Left hand part type LHP Name Right hand part type RHP VarName String VarValue Integer oe oe used to indicate the index for next statement to execute normally first ProgCounter is used but when conditional statement like if then else is used the first ProgCounter is for positive evaluation in if and the second ProgCounter is for the negative evaluation in else type NextProgCounter ProgCounter ProgCounter oe oo oo oe oe oo oe oe Statement definition type Stmt Name TypeOfStmt LHP RHP NextProgCounter Figure 37 Statement type declaration Finally the Program Memory State and the SystemState are declared as shown in Figure 38 5 Program declaration type Program List Stmt ProgCounter 5 Memory State declaration Variables Low Input High Input type MemoryState Variable
101. n let prog s 4 in as nth will be used of the list before proceeding gt s 4 2 then ls SystemState SystemState Specification it is required to confirm the length Isabell 100 let stmt nth prog 1 prog 2 in 5 Handle read low statement if stmt 2 ReadLow then 5 Read from low input and assign to variable specified by LHS let new mem read low func stmt 3 vars inputLow inputHigh in Update prog state assign next program counter let new prog prog 1 stmt 5 1 in new mem 1 new mem 2 new mem 3 new prog 6 Handle read high statement else if stmt 2 ReadHigh then 5 Read from high input and assign to variable specified by LHS let new mem read high func stmt 3 vars inputLow inputHigh in 5 Update prog state assign next program counter let new prog prog 1 stmt 5 1 in new mem 1 new mem 2 new mem 3 new prog Handle write low statement else if stmt 2 WriteLow then There is no output implemented so nothing specific to do for write Update prog state assign the next program counter let new prog prog 1 stmt 5 1 in vars inputLow inputHigh new prog 6 Handle write high statement else if stmt 2 WriteHigh then There is no output implemented so nothing specific to do for write Update prog state assign the next program counter let new prog prog 1 stmt 5 1 in vars inputLow inputHigh new prog 6 Hand
102. n of all actualized flows from system operations Flow related type ModeOfFlow Read Write type FlowModeSet Set ModeOfFlow 5 Flow effect amp Set of all possible flow effects type Flow subj Subject obj ResourceExt fset FlowModeSet Defines all effects associated with an operation transform type Transform Set Flow type MM Set Transform Figure 77 Definiton of Flow FlowEffect Transform and MM A flow policy defining the least privilege flow control between Subject and ResourceExt and the block to block flow control between B ocks will be defined next The two flow policies are orthogonal i e a flow allowed in one may not necessarily be allowed in the other policy The Policy object is defined to be made up of two matrices as shown in Figure 78 5 Policy is preset and passed in during initialisation type Policy srm SRMatrix bbm BBMatrix Figure 78 Definition of Policy The least privilege flow control is defined by a subject resource matrix SRMatrix which contains a collection of flow tuples depicting allowed flows between a Subject and a ResourceExt defining the least privilege flow policy The function SR as 65 shown in Figure 79 extracts out from the SRMatrix the tuple corresponding to the Subject and ResourceExt specified Each SRMatrix should contain at most one flow tuple corresponding to each Subject and ResourceExt pair as ensured by the axiom SRSingleE
103. ncluding exception handling capturing of state and state transitions and output handling 18 Of special relevance in the context of the thesis regarding the construction of security models is the use of Monads to represent state transitions Programs written in functional style can make use of Monads to structure procedures that include sequenced operations or to define arbitrary deterministic control flows like handling concurrency continuations or exceptions 18 Of special relevance in the construction of security models is state transition The usual formation of a Monad is known as a Kleisli triple and has the following components 18 a A type constructor M that must fulfill several properties which make possible the composition of functions that the user values from the Monad as their arguments so called monadic functions It defines how the 14 monadic type can be obtained from one or more specific underlying types If M is the name of the Monad and is a data type M is the corresponding type of the Monad A unit function mapping a value in an underlying type to a value in the corresponding monadic type The function is usually called return and has the polymorphic type a M a A binding operation of polymorphic type M a a M b Mb The first argument is a value in a monadic type the second is a function which maps from the underlying type of the first argument to another monadic type and the r
104. ned to ensure separation policy regarding internal resources Due to time constraints this is not covered in this thesis An alternative approach would be to conduct a comprehensive covert channel analysis of the system and specifications to provide the evidence for separation of internal resources In the modeling the team has not attempted to build an abstract model and a final target model as has been performed by DeCloss 2 Morphism is supported and is a strong feature in Specware and it may be useful if the team first develops a canonical abstract security model which is refined only in its subsequent target model This will allow the reuse of the specification for other models and also allow modellers to focus on only the areas they want to focus on at the point of modeling For our current model additional suggested follow up specification work includes specification of semantics of read op and write op which currently are abstract operations which result in changes in the subject and object memory respectively It is also important to note that the use of if then else Figure 94 constructs in our model particularly in the transition operation may make subsequent refinement attempts more 81 difficult It would be convenient if it can be replaced with a chained predicate construct Figure 95 prevalent in functional programming The team briefly investigated how to replace the construct as c is a Monadic State Transition functi
105. ntrySubjObjPair If the tuple is not found in the SRMatrix it is assumed that no flow is allowed between that Subject and ResourceExt pair This is equivalent to an empty fset for the Subject and Resource FRR RRA OK UK BORA KER KR RR ED CO KC OK GUERRE EC AIR KOR RRR CON BERK RRR ODORE AOR KG KR KK KOR UN UO E OK Dok eoe Subject to Resource Policy and Flows Check is based on the policy matrix specified RRR AAR OK UK PERAK OE OK KER RRA NOR RE RRR KR OR UK OON A RO OUR OROCORUN KERRIER RRR RRR KR RRR IER RK KC 5 Subject to Resource flow record type SRMatrix Set Flow oe oo returns the modes of flow allowed between a given subject and resource in a given SRmatrix oo oe op SR pol SRMatrix subj Subject extobj ResourceExt FlowModeSet let bset pol fn i gt i subj subj amp amp i obj extobj in case single bset of tru gt theMember bset fset false gt empty axiom SRSingleEntrySubjObjPair is fa pol SRMatrix subj Subject extobj ResourceExt let bset pol fn i gt i subj subj amp amp i obj extobj in single bset empty bset Figure 79 Definition of SRMatrix Block to block flow control policy is defined by the BBMatrix in Figure 80 BBMatrix contains a set of BBRecord tuples which specify the set of flow modes allowed between a source block and a destination block The operation BB locates the BBRecord inside the BBMatrix for a specified
106. o an Abstract Canonical Model and a Refined Mi Od els iscissts cicsscscsessscsavecdascevcapuntevedassbasensecsessesdncensonvtse 88 3 Code Generation from a Verified Model using Specware 89 4 Running Specware Isabelle on Alternative Platforms 89 APPENDIX A 6610 EXAMPL or 91 A HASKELL EXAMPLE 19 iieiicic cce erten ore road a pe Peer peo ense ro sor oth end ehe 91 B CORRESPONDING EXAMPLE IN SPECWARE ee ee eere eene 92 APPENDIX B BLP PROPERTY MODEL ceto n eae crop a pee su eva S oeae p ena 95 A TYPEDEESPEGC SW scsi cx tessssccaascs onein rn ibi n enc Lacu ep soda aE Coo vean 95 B MEMORYSPEC SW 5 teri eoe etit o reete ede pra oni Cedo Mae eiu ere apio ir ec e ie estaS 96 C STATEMENISPEC SW iieeceiesehtbteceseute eese teet eeu DM baee ee ree ic e oiabb evan 97 D END TS PE CSW C 100 E FILESYSTEMSPEC SW ietetesiesmen debet tvescioserducesceueaoaretaneqatiocsdonewiees 100 APPENDIX C BLP MODEL Pc kassia 105 A BLPISW ect ATE A Merit to Da peu uice eio Ma eod Mic TDo ap SUD P Craco Dea e 105 APPENDIX D LPSK MODBL eoo ete ndo euo ino epuuo onere sn eto cv neun oen toa vedo 111 A LPSK SW E EE E E E ES 111 LIST OF REFERENCES sisssscescsssesceneieacesacnstcavesscatcaste nssuasncacecisectteps vacatencesiieswiucteieivustoxes 123 INITIAL DISTRIBUTION LIST eseeeossesossoesesossossesocssssoseossesocsossesocsossesoosossossossesocsossesooss 125
107. odel have been documented and discussed in the previous section The most important takeaway was that the proving on Isabelle platform is not trivial and would take more than just simple predicate and theorem proofing knowledge and basic understanding of Isabelle to complete the proof Experience would be another key asset as we saw how the Kestrel 56 team brilliantly guided Isabelle across many of the proof obligations The team realized that it would not be possible to amass such technical expertise and experience within the time constraint of our project Focus will be placed instead on completing the modeling of LPSK F MODELING LPSK IN SPECWARE 1 Model Description A separation kernel refers to hardware and or firmware and or software mechanisms whose primary function is to establish isolate and separate multiple partitions and control information flow between the subjects and exported resources allocated to these partitions The goal of the separation kernel is to virtualize and allocate shared resources such that each partition encompasses a resource set that appears to be isolated from the rest The Principle of Least Privilege PoLP is a foundational element in the design of high assurance systems In the context of computing it requires that every module a process a user or a program must be able to access only such information and resources that are necessary for the purpose it is built for It allows for the confinemen
108. of our model some corresponding to those defined previously for the BLP example can now be formulated The first operation in Figure 90 secure write transition states that an invocation of write op will result in a change in the object memory The actualization of the flow from the Subject to the object ResourceExt implies that the flow is currently enabled Correspondingly the secure read transition states that an invocation of read op will result in a change in the Subject memory In this case the occurrence of the flow from the object to the Subject implies that the flow is enabled i e the flow is present inside the access tuple set at the point of invocation of read op These two operations are essential as they define that a flow actualized by a State change must be one that is enabled for a system to be secure The securestate predicate checks to see if the state of the system is secure based on the contents of the access tuple set A state is defined as secure if all the elements of the access tuple set satisfy access secure The theorem EmptySecure describes that a system state whereby the access tuple set is empty is secure The StateMonad currently accessible predicate will always return a false for all invocations and no flow will result based on our defined model 76 The next theorem SecureSystem states three properties for a System to be secure Firstly if the current state is secure a transition will result
109. on that returns a StateMonad Boolean rather than just a Boolean and the completion of this effort was left for future work if a amp amp b thenc Figure 94 if then else construct a amp amp b amp amp c Figure 95 Chained predicate construct For the model to be useful additional work is needed to verify it discharge its proof obligations and attempt proving them using a tool like Isabelle in order to prove the security properties related to the model Subsequently execution codes may also be generated directly from the model It is important to note though that the use of Set may potentially hamper the translation to execution code as sets may be infinite When such refinement to executable code is desired FiniteSet should be used in the specification in place of Set Specware does not support the declaration of model level variables and parameters unlike other specification languages like Prototype Verification System PVS As a result for every defined axiom or theorem operation level parameters have to be redeclared and used making the specifications more cumbersome and less flexible 82 V RESULTS AND ANALYSIS It is demonstrated in this thesis that the translation from Specware to Isabelle can be seamlessly achieved using the Specware to Isabelle Translator The team has also completed the building of a LPSK model using Monads and the Set base library released in Specwar
110. otality of bbase amp Note that transform flows are a set of flows while depicts a flow from a block to another block derivebbflowset extracts all possible subject to resource flow sys systemflows derivebbflowset bbase bcontra amp amp PO blkset bbase amp amp fa rs Resource r Resource f Set ModeOfFlow low must be allowed in bcontra but not bbase BB bcontra RB rs RB r amp amp oe oe ES Fh low must be allowed in SR SR sys pol srm rs r amp amp oe oe I J Hh lt oe Upon adding the equivalence of the flow from rs to r partial ordering no longer holds for the block set oe new bbase oe oe PO blkset bbase bl getBlock sys blocks b2 getBlock sys blocks RB r fset f oe rs must be a trusted subject gt exported rs amp amp active rs amp amp trusted rs 3 Dis Figure 93 Definition of Trusted Partial Ordering cussion and Lessons Learned Building of the LPSK model specification started only after our visit to Kestrel in late October 2008 The Kestrel team recommended the use of the Specware Set Base Library instead of the List Base Library which the team had along with DeCloss 2 in a previous project thus far depended upon The Set Base Library was introduced only in the latest version of Specware version 4 2 5 which was officially released in November
111. p add MonadBLPSimpleExampleExceptions securestate p def mem def qed Figure 14 Example of Isar proofs in Isabelle D SETUP OF DEVELOPMENT ENVIRONMENT IN FEDORA 8 We are running Fedora 8 in VMware Workstation on a Windows Vista machine The license for the VMware Workstation and the image for Fedora 8 are obtained from the CISR lab The following software are required in Fedora 8 for the Specware and Isabelle development environment XEmacs version 21 5 28 5 e Isabelle 2008 version Specware version 4 2 2 1 XEmacs Version 21 5 28 5 XEmacs can be installed using the yum command in Fedora Internet access must be available for the Fedora 8 machine before yum can download and install the XEmacs Figure 15 shows the command to install XEmacs root localhost yum install xemacs Figure 15 yum command to install XEmacs 20 2 Isabelle 2008 Version The following files are required for the Isabelle 2008 installation Isabelle2008 tar gz ProofGeneral tar gz e Polyml_x86 linux tar gz e HOL_x86 linux tar gz Figure 16 shows the installation instruction for Isabelle 2008 Installation of Isabelle HOL on Linux x86 and x86 64 works by downloading and unpacking the relevant packages Here the installation location is usz 1oca1 but any other directory works as well tar C usr local xzf Isabelle2008 tar gz tar C usr local xzf ProofGeneral tar gz tar C usr local xzf polyml
112. pabilities 2 Specware has since included a translator to translate a Specware specification to an Isabelle Specification Isabelle is a generic proof assistant that allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus 5 We are demonstrating in this thesis that a specification in Specware can be translated to Isabelle using the tool We will explore though not in depth some proving capabilities of Isabelle A number of simple proofs will be demonstrated in this thesis State changes are common in most security models We are exploring the use of a recursive function and Monad to represent state changes Monad was mentioned in DeCloss s Thesis 2 as future work and we will explore and demonstrate how state changes can be represented using State Monad This thesis presents our encounter and experience with security modeling using the latest version of Specware and auto proving with Isabelle and our follow up work on Decloss s Thesis We begin by first presenting a brief overview of Specware its specification language MetaSlang and Isabelle We then describe our approach in 1 learning the concepts of security modeling and modeling and discuss the intermediate and final models we built We then conclude with our analysis of Specware and Isabelle and present our learning experience together with recommendations for future work Il BACKGROU
113. pair of source and destination and returns the set of allowed flows from the source to the destination For any defined Block a a flow from any block to itself is always allowed This is defined in the axiom BB FLOWS BLOCK INTERNAL ALLOWED 66 oe oe Block to Block flow record Represents flow of information between blocks BBMatrix contains tuples depicting a Set of FlowModes between 2 blocks If a BBRecord linking 2 blocks is not found no allowable flow is allowed source is bl dest is b2 type BBRecord bl Block b2 Block fset FlowModeSet type BBMatrix Set BBRecord oe oe oe oe oe oo oo oe BERRA ERR ROARK RRR KER FUE OK ORORUK RRA OU KIRK RAR SK E OE UK ON OK IG KC ORO OE IK RRR ER GE UE OK COR OK ON OK RK FOR Block to block Policy and Flows Check is based on the policy matrix specified REIKI RABE EERE ROR OR OK OK OK ox OK POE ON LR Oe s ene ce kc c deae o OK COGOR DECUS OK OK oe Retrieve allowed flows modes from block a to block b from given policy matrix op BB bb BBMatrix a BlockId b BlockId FlowModeSet let bset bb N fn i gt getBlockId i bl a amp amp getBlockId i b2 b in case single bset of bra gt theMember bset fset false gt empty oe No other blocks exist other than those in sys blocks 5 All blocks can both read and write to themselves axiom BB FLOWS BLOCK INTERNAL ALLOWED is fa sys System a Block let bid getBlockId a in
114. ples 48 E MODELING BLP IN SPECWARE i Model Description The concept of mandatory access controls was formalized by Bell and LaPadula in a model commonly bearing their name 10 Numerous variations of the model have since been published but only a very simplified version will be considered in the context of this paper for the building of a sample security model using Specware Mandatory access control policy for confidentiality is based on security labels attached to subjects and objects Subjects represent the entire entities of a computer system such as processes A label on a user is called security clearance and a label on a subject or object is called a security classification The label space forms a lattice and two labels are related by a dominates relation Typically enforced during login a supporting policy ensures that the subjects acting on behalf of the users have labels that are dominated by the user s clearance A user with a secret clearance can run the same program as a subject labeled secret or as a subject labeled unclassified assuming the program is labeled unclassified Even though both the subjects run the same program on behalf of the same user they obtain different privileges due to their security labels This thesis addresses the security of subjects and objects and the modeling of the supporting policy is left for future work Mandatory access BLP rules can be expressed as follows with SecLabel re
115. presenting the security label of the indicated subject or object Simple security property Subject s can read object o only if SecLabel s dominates SecLabel o property Subject s can write object o only if SecLabel o dominates SecLabel s Integrity policy is outside the scope of this thesis 49 2 Specware Model a Required Library The Specware General library version 4 2 5 is imported to support on the Set and Monad types as shown in Figure 55 import Library General Figure 55 Importing Specifications from General Library b Type Description For this example we declare classification labels of Top Secret Secret Confidential and Unclassified to represent SecLabel which is typically how confidentiality levels are defined in the military world In Figure 56 a Resource is declared to have a name and a label Both Subject and Object are of the type Resource The Mode represents the type of access 5 Defining 4 types of security labels type SecLabel TS label S label C 1abel U label Resource Related Types type ResourceName String type Resource name ResourceName label SecLabel type Subject Resourc type Object Resourc Access Mode type Mode Read Write Figure 56 Security Label Access Mode and Resource type Declarations c Transactions Next two transform types are defined as shown in Figure 57 which represent the
116. primary security mechanisms of the BLP model The first MakeKnown 50 adds a mode of access expressed in the form of an AccessTuple for a subject to an object while the second Terminate removes a mode of access for a subject to an object 5 Current Access Transform Type amp Access Tuple type ATTransaction MakeKnown Terminate type AccessTuple Subject Object Mode Declaration of Access Tuple and Transform Type Figure 57 d Input The Input to a transformation is declared in terms of the AccessTuple and ATTransaction as shown in Figure 58 Input Types type Input AccessTuple ATTransaction type InputList List Input Figure 58 Declaration of Input Type e State The SystemState represents the current modes of access of Subjects to Objects A StateMonad is defined for the SystemState along with the corresponding return and monadBind functions as shown in Figure 59 9 9 6 State and StateMonad type State Set AccessTuple Stat type SystemStat oo OO op op a return a b StateMonad b f y stl type StateMonad a SystemStat Monad return and bind functions x a monadBind fn st gt let gt a SystemState fn st x st f a gt StateMonad b StateMonad a m1 StateMonad a ml st in y stl Figure 59 Declaration of State Related Types State Monad and associated functions 51 SecLabel is defined in a LinearO
117. r an access is allowed based on an input access tuple op access_allowed SRMatrix BBMatrix Subject ResourceExt FlowModeSet gt Boolean def access allowed srm bbm subject object am am lt SR srm subject object amp amp am lt BB bbm subject blkid object blkid Op access secure SRMatrix BBMatrix Flow gt Boolean def access secure srm bbm subj subject obj object fset am access_allowed srm bbm subject object am Figure 87 Security predicates The transition operation which transits the state based on an nput object and the system policy is next defined The nput object is made of two attributes an AccessTuple detailing the subject object and flow mode requested and an ATTransaction flag indicating the type of transaction sought by the caller More detail of the different ATTransaction types and their effects on the state are given in Table 3 The corresponding Specware definition is given in Figure 88 Transaction Description Type Make Known Making a request for access as described by the specified AccessTuple An entry is added to the AccessTuple table if the access is allowed by policy and the access tuple is not currently present in the set of AccessTuples in system state Accesses have to be made known before ReadExternal and WriteExternal operations may be made Terminate Making a request to terminate all accesses as specified by
118. r use with the use of Set as can be shown in the BLP example The State originally represented as a List and manipulated by List operators is amended to be represented in Sets The resultant specification looks much more concise and cleaner but it is later found that the Sets being represented as predicates lack the useful manipulators available in Lists Use of pattern matching Although not explicitly and extensively documented pattern matching is a strength in the Specware language and the Kestrel team recommended its use It is important to note though that its use results in terse expressions which though concise may not be as readable to consumers of the specification Use of Monads The team verified with Specware the correct and apt use of Monad in our BLP example While questioning the relevancy of Monad use for such a simple example the 47 Kestrel team affirmed that our use is appropriate and it correctly encapsulates the sequenced operations and imperative code inside the transition operation The use of Monad though does not make subsequent proofing easier It only performs a certain state of encapsulation and bookkeeping It is further verified that Exception Monads may not be directly applicable and useful for our simple model 3 General Proving Strategy The Kestrel team offered some general advice on our specification to facilitate proofing First it is recommended that the types and operations must be defin
119. rder The operation dominates in Figure 60 defines the Linear Ordering with Top Secret Label dominating Secret Secret dominating Confidential and Confidential dominating Unclassified The dominance relationship is transitive as a result of linear ordering For example 7S abel dominates C label in this case due to the fact that the TS label dominating S label which dominates C abel dominates function a security label dominates another which is of equal or lower classification op dominates LinearOrder SecLabel the dominates dominates TS label S label amp amp dominates S label C label amp amp dominates C label U label Figure 60 Definition of dominates operation Security Property Predicates on Sets are used to assess if an access or a state is secure An access tuple is secure only if the label of the subject dominates that of the object for the case when the access mode is Read and vice versa for the case when the access mode is Write Since this expresses essentially the set of all possible secure tuples we can express a Secure State as one which is a subset of this as illustrated in the securestate predicate defined in Figure 61 Helper functions for the Current Access are also defined as shown in Figure 62 52 oe specified acce Op access secure def access secure Checks if a subject can access an object using a ss mode based on BLP rules Acce
120. re 32 Initial type declaration type Name String type Value Integer type Index Nat type ProgCounter Nat Figure 32 Initial type declaration 35 The label is declared as high or low as shown in Figure 33 type Label High Low Figure 33 Label type declaration Variables are declared as a list of tuples as shown in Figure 34 The tuple consists of Name Value and Label Variable declaration type Variable Name Value Label type Variables List Variable Figure 34 Variables type declaration Input is declared as a tuple as shown in Figure 35 The tuple consists of a list of values and an index The index will indicate the next value to be read from the input list Input declaration type Input List Value Index Figure 35 Input type declaration Types of statements that are supported in this model include ReadLow ReadHigh WriteLow WriteHigh Assignl Assign2 and Stop as shown in Figure 36 Assign is being represented by Assign and Assign2 where Assign represents assigning a variable to another variable and Assign2 represents assigning a constant to a variable oe oe Statement declaration assignl variable name variable name eg a b assign2 variable name value eg a 5 type TypeOfStmt ReadLow ReadHigh WriteLow WriteHigh Assignl Assign2 Stop Figure 36 Type of state
121. ried out at the requirements and code level as performance of formal methods drive up the cost significantly To reduce cost the intensive mathematical study of the key programs approach focuses only on the difficult and problematic part This however carries the danger that something of security relevance might be overlooked unless the security functions have been factored into a small number of underlying components Automated verification systems or theorem provers would be useful in formal verfication as they can greatly increase the efficiency and productivity The general complaint though is that they are time consuming to use costly and to date they are limited in their ability to be fully automated Most require an untrival level of guidance from the human operator to complete the proofs Successful verification though will give users the assurance that the software will work and behave as specified which is crucial in security and safety critical software The Common Criteria imposes the requirement that any system requiring a high level of trust e g Evaluation Assurance Level 7 or EAL 7 must undergo a rigours life cycle including the use of formal verification of its security properties 9 Formal verification is incorporated in the development life cycle to ensure that the system is correct While necessary for high assurance systems the level of effort associated with manual verification can be unreasonably huge due to larg
122. rresourceMem lt get resource memory at subj return x memsect Set Bit memsect lt b4resourceMem amp amp memsect lt at obj rscmem amp amp memsect afterresourceMem else return false WriteResourceExt gt curr currently accessible at if curr then b4objMem lt get resource memory at obj write op at subj at obj afterobjMem get resource memory at obj return x memsect Set Bit memsect lt b4objMem amp amp memsect lt at subj rscmem amp amp memsect lt afterobjMem else return false Figure 88 Definition of transition operation Security Theorems In Figure 89 the top level encapsulating operation which initializes the system and furnishes an input list is defined This may be useful in formulating general theorems involving an arbitrary number of inputs e g an InputList of arbitrary length and results in the state resulting from the nputList transition and a list of Boolean results corresponding to the success of failure of these transitions 75 type InputList List Input op evalProgram InputList System StateMonad List Boolean def evalProgram inputs sys case inputs of gt return inp r inputs gt rl transition inp sys res evalProgram r inputs sys return rl res Figure 89 Encapsulating function A few theorems
123. rte PUES EE oed PPM EUR pon 26 2 UNI MEN 27 3 Traffic Light as a List of Colors eese eee erue eere ener 27 4 Traffic Light as a State Tuple ce eee eee eee eee ee eee eese co 31 5 Discussion and Lessons Learned cccccccsccsccscsscccescsecsceseesees 33 C MODELING BLP PROPERTY IN SPECWARE eee eee ee etn eee 34 1 han DGS CEU IONE Ser cast coins caseetegxtacermoeaters 34 2 Specware MOE siscc ccsesesctuiuecisicepesaeancaesceibepeesoaseaecentucuwsucavsnetsantennenee 35 a Type Definition TypeDefSpec sw e eeeeee esee enne 35 b Memory Manipulation MemorySpec sw eee 38 c Support Functions for Statement Execution StatementSpec SW ieieeecssetea tt esse endet edant aa su aee eas ah eene doute 39 d Initialize Specification InitSpec sw eese 41 e Main Specification FileSystemSpec sw eese 41 3 Discussion and Lessons Learned eeeeeeeeeeeeeeeeeeeeee 44 D LESSONS LEARNED AT THE KESTREL INSTITUTE 46 1 Specware IVIOCEl aces cscassescasshednccess dcewcesshcceceaanieecaneaccewes caceeeenesnentenneanens 46 2 Useot MonadsS x easccsesesistskeciieshicegsubicctsscubesacsnceteosdanessaabesoouadcapeeadsnceses 47 3 General Proving Strategy sioe eren ono eter cdeccedenucicoveddoedcecasteceventecsers 48
124. rtial ordering bcontra ERK RAK KR AK KIA ERE OR OK CECK OR DE ON OR RK KR KIRK OROK CK OK KIRK ACKER CK UK KK RK RANK KIRK e Ree ek ERR Y theorem TPO is fa sys System bbase BBMatrix ex blkset BSet bcontra Set BBRecord oe System Transform flows will be totality of bbase amp bcontra Note that transform flows are a set of flows while BBRecord depicts a flow from a block to another block derivebbflowset extracts all possible subject to resource flow oo oe oe oe oe oe oe oe oo sys systemflows derivebbflowset bbase bcontra amp amp 119 PO blkset bbase amp amp fa rs Resource r Resource f Set ModeOfFlow oe Flow must be allowed in bcontra but not bbase lt BB bcontra RB rs RB r amp amp Hh oe Flow must be allowed in SR f lt SR sys pol srm rs r amp amp oe Upon adding the equivalence of the flow from rs to r partial ordering no longer holds for the block set and new bbase oe oe o 2 PO blkset bbase lt bl getBlock sys blocks RB rs b2 getBlock sys blocks RB r fset f rs must be a trusted subject gt exported rs amp amp active rs amp amp trusted rs oe PEPE KERER KERR RR KER KDE GR UK KIRIK RRR LAR KK UK FERAL SERIE KICK LER KR KREE REE KR KBR ARK Security Theorems KOKSKOKCKUKOKKOKUKUKCKOKCK AAA IIE RAK ION ARE I RRR RK EK KORE IR KR ROR KE TK KER ROE
125. s Input Input System state declaration Variable Low Input High Input Program type SystemState Variables Input Input Program Figure 38 Program Memory State and System State type declaration 37 b Memory Manipulation MemorySpec sw All the functions to manipulate the memory state of the model are located in the MemorySpec sw These functions include read_low read_high find_variable and update_variable They are used by functions in StatementSpec sw The read_low definition will read the next input from low input increase the index of low input and return the new memory state and the read value from low input The definition is shown in Figure 39 oe oe Read from the low input list based on the current index Increment Index Returns the value read oo oo oe oe op read low MemoryState MemoryStateValueTuple def read low mem state let read value read inputLow mem state in let updated input stream mem state 2 1 succ mem state 2 2 in let updated memory mem state 1 updated input stream mem state 3 in updated memory read value proof Isa simp end proof Figure 39 op read low definition The read high definition is similar to read low definition except that it will read from the high input and return the value from high input The find variable definition will find the variable from the variable list and return the variable tuple The re
126. s true for the case when the current attempted access is already in the current access set In this special case the result of adding the current access to the set will remain as S In the case where the current access is not secure it is not added to the Current Access set oe Theorem stating change of state after a MakeKnown transform type state will be a subset of the original state theorem transition MakeKnown secure is fa S State S State at AccessTuple access secure at gt transition at MakeKnown S 2 S at oe theorem transition MakeKnown not secure is fa S State S State at AccessTuple access secure at gt transition at MakeKnown S 2 S Figure 65 Sub theorems for MakeKnown A similar theorem is formulated for the Terminate transaction as shown in Figure 66 For this case terminate involves removal of a tuple from the current access set if it exists As such the resultant State should be a subset of the original State Theorem stating change of state after a terminate transform type New state will be a subset of the original state theorem transition Terminate subset eq is fa S State S State at AccessTuple transition at Terminate S 2 lt S oe oe Figure 66 Sub theorem for Terminate 55 Next the theorem transition_state_secure is formulated as in Figure 67 This theorem states that given an initial secure state for any input the state
127. sion The Graphical User Interface also appears slightly unstable and incessant refreshing resulting in blinking of windows was occassionally encountered Specware and Isabelle can alternatively be run on Mac OS environment but this is not explored in the project It is also possible to run Isabelle on Windows using Cygwin E SETS The newly released Set library provides a convenient and more natural way for modeling set relations and collections as compared to the use of List In the LPSK model the team used the Set library extensively to model the key model components and their relationships Resource Block policy matrices BBMatrix and SRMatrix and the access matrix AccessTuple are implemented as sets in our model Set predicates are employed in many of the axioms and theorems formulated Appropriateness and correctness of use of the Set Library inside our model could be verified when accompanying documentation and examples become available F MONADS Monads allow the embedment of an imperative programming element into functional programming code but it does not seem to simplify the proving process on Isabelle The concept of Monads is not easily grasped and not much supporting documentation exists in the Specware user manual The team was able to learn to use Monads from the visit to Kestrel and the many available Haskell resources on the web 85 and from building simple examples emulating the Haskell ones widely available on the
128. ssTuple gt Boolean subject object case access mode of Read dominates subject label object label Write gt dominates object label subject label op securestate S State Boolean S lt access_secure op property St def property s ate gt Boolean securestate s access_mode Figure 61 Definition of security predicates to check security property oe oe Auxillary Functions for Current Access to check if contains a tuple Also for adding and removing tuples from Current Access Table op currently accessible at AccessTuple StateMonad Boolean fn S State gt at in S S op addAccess at AccessTuple StateMonad fn S State gt S at op removeAccess at AccessTuple StateMonad fn S State S at Figure 62 Definition of manipulators of Current Access g State Transition Transformation Figure 63 specifies the possible state transformations As discussed above two transform types are defined The first MakeKnown adds a mode of access expressed in the form of an AccessTuple for a subject to an object while the second Terminate removes a mode of access for a subject to an object evalProgram takes in a list of input and runs transition on them The results are returned in an output list 53 oe This corresponds to the main function performing the statement It wi
129. t index Increment Index Returns the value read op read high MemoryState MemoryStateValueTuple def read high mem state oe oe oe oe let read value read inputHigh mem state in let updated input stream mem state 3 1 succ mem state 3 2 in let updated memory mem state 1 mem state 2 updated input stream in updated memory read value proof Isa simp end proof 5 Find the variable from the variable list 5 based on variable name and return the variable op find variable Name MemoryState gt Option Variable def find variable var name mem state find fn i compare var name i 1 Equal mem state 1 proof Isa simp end proof 9 o 6 Update the varibale with the new value op update variable Name Value Label MemoryState gt MemoryState def update_variable var_name var_value var_Label mem_state let new_var insert var_name var_value var_Label filter fn i compare var name i 1 Equal mem state 1 in new var mem state 2 mem state 3 proof Isa simp end proof endspec C STATEMENTSPEC SW oe oo This Specification contains all the functions that are required by the BLP property model to execute the different type of statements Statement spec oo oe oo oo import MemorySpec MyMemory GT Greater than 97 ess than Greater or Equal Less than or Equal oe p LE Ed H
130. t of damage when corruption of components occur and as the privileges afforded each component will be minimal security analysis of the TOE Security Functions TSF is less complex TSF is consequently more evaluable and accountable The Center for Information Systems Security Studies and Research CISR created the Trusted Computing Exemplar TCX project to illustrate how trusted computing systems and components can be constructed The project is developing a high assurance Least Privilege Separation Kernel LPSK with a hosted trusted application as a reference implementation for trusted computing The paper A Least Privilege Model for Static Separation Kernels 12 describes a core Formal Security Policy Model of a separation kernel that enforces the Principle of Least Privilege Previous students from NPS have specified elements of similar models using PVS 1 Specware 2 and Alloy specification languages 3 DeCloss s model in 57 particular was created using an earlier version of Specware version 4 1 3 In his paper as part of the scope for future work he suggested the use of Monads to represent state in Specware and enhancement of the model he built in his thesis to include requirements for the TCX LPSK such as incorporating a notion of initialization of the policy tables within the model and the modeling of a trusted partial ordering on the flows between blocks for the identification of trusted subjects The
131. talling the Specware version 4 2 2 in Fedora 8 java xcb xlib c 50 xcb xlib unlock Assertion c gt xlib lock failed Figure 17 xcb_xlib error while installing Specware version 4 2 2 in Fedora 8 21 A possible solution to this error is to update the libxcb to version 1 0 4 before proceeding with the Specware version 4 2 2 installation The libxcb can be updated using the command yum update libxcb At the time of this writing version 1 0 4 is not available for update in Fedora 8 A number of manual configurations are required to get Specware version 4 2 2 to run on Fedora 8 platform This list of manual configuration is listed in Table 2 SN Manual configuration Comment Delete the line SHERE Find_SBCL from Specware and SpecwareShell in opt Kestrel Specware 4 2 2 directory Delete the following lines from XEmacs_Specware in opt Kestrel Specware 4 2 2 directory Try to find lisp executable if z SLISP then for L in Applications sbcl bin sbcl usr local bin sbcl SHOME bin sbcl bin lisp do if x L then LISP L break fi done fi if z SLISP then echo Failed to act no LISP executable found 2 gt amp 1 exit 1 fi if x SLISP then echo Failed to act LISP is not executable 2 gt amp 1 exit 1 fi SBCL is no longer required by Specware Comment out the line x symbol specware from files el in opt Kestrel
132. te 5 system state transition op transition SystemState gt SystemState def transition s 5 as nth will be used it is required to confirm the length 5 of the list before proceeding else Isabell if length s 4 1 s 4 2 then let vars s l in let inputLow s 2 in let inputHigh s 3 in let prog s 4 in let stmt nth prog 1 prog 2 in 5 Handle read low statement if stmt 2 ReadLow then Read from low input and assign to variable specified by LHS oo oe oo let new mem read low func stmt 3 vars inputLow inputHigh in Update prog state assign next program counter let new prog prog 1 stmt 5 1 in new mem 1 new mem 2 new mem 3 new prog 5 by defualt return the current state for unknown statement else s proof Isa simp end proof Figure 47 Partial op transition definition The BLP property is defined in the property definition shown in Figure 48 Only if the statement is doing a WriteLow and the label of the variable to be written to Low is High then the definition will return a false 42 59 check the system state for writing high to low BLP property op property SystemState gt Boolean def property s as nth will be used it is required to confirm the length of the list before proceeding else Isabell if length s 4 1 s 4 2 then let stmt nth s 4 1 s 4 2 b will return false only if the statement is writelow and the label of the variabl
133. team s first attempt at modeling the notion of a state which essentially is the color of the light and the state change function A simple theorem labelled light change has been formulated as an illustration Its proof obligation is discharged for proving in Isabelle via the Specware to the Isabelle Interface and proven successfully The translation looks simple but in fact took substantial effort as the team was new to 33 Specware Isabelle and also to the Specware to Isabelle Interface Whenever a problem was encountered in the proofing of the outputted Isabelle specification it was not easy to determine if the problem lies in our model or in the Isabelle Specware translation For example a few of the problems were related to the use of the Nat and nt types due to the additional obligations generated for the former type As the team worked with the model and proofiing we realized increasingly that a working knowledge of theorem provers and Isabelle would be needed to guide the proof and troubleshoot any problem that may arise due to the translation Having got a first taste of Specware and Isabelle the team proceeded to build the first security model to model BLP property in Specware C MODELING BLP PROPERTY IN SPECWARE 1 Model Description We are creating a security model based on the Security Domain Model 25 This model consists of two inputs a memory and a list of program statements as shown in Figure 31 Computer Sys
134. tem List of variables List of high Main Program Program List of low Statement inputs Figure 31 Computer system block diagram The high inputs represent input with high label while the low input represent input with low label The label of the variable takes the label of the source which can be 34 high input low input another variable or a constant low label The types of statements supported in this model are read write and assign The security property the model is checking is property no write down of BLP 2 Specware Model The Specware model is being broken down into the following Specware Specifications TypeDefSpec sw the specification file where all the required type definitions is located MemorySpec sw the specification file where all the functions that manipulate the memory state variable high input and low input is located e StatementSpec sw the specification where all the functions that FileSystemSpec sw required to execute the statement assign read and write e InitSpec the specification where the initial state of the system is being defined FileSystemSpec sw the main specification of the model which includes the state transition property check and the theorem a Type Definition TypeDefSpec sw All the required type declarations by the model are placed in the TypeDefSpec sw For easy readability some initial types are declared as shown in Figu
135. temState Stat type StateMonad a SystemStat gt a SystemState op dominates LinearOrder SecLabel the dominates dominates TS_label S_label amp amp dominates S_label C label amp amp dominates C_label U label proof Isa BLP__dominates_subtype_constr apply simp add BLP dominates def apply rule tac Q Order linearOrder p in thelI2 apply auto simp add BLP dominates Obligation the end proof oe oe For the state to be secure all tuples inside the state must satisfy the tuple is secure property Initially the access tuple list is empty oe oe oe oe oe oe oe oo modebased on BLP rules Op access secure AccessTuple gt Boolean def access secure subject object access mode 105 Checks if a subject can access an object using a specified access case access_mode of Read gt dominates subject label object label Write gt dominates object label subject label op securestate S State Boolean S lt access secure oe oe Checks to see if the tuple specified in inside the current state Returns true if tuple exists false if tuple does not exist oe oe op a return x a StateMonad a fn st gt x st op a b monadBind ml StateMonad a f a StateMonad b StateMonad b fn st gt let y stl ml st in f y stl 6 Accessory Functions to retrieve and set values inside states op currently accessible
136. the AccessTuple The mod field is ignored and all accesses related to the subj and obj specified are removed 13 Read External Making a request for the subj to read the obj specified The mod field is ignored and we define that some state change has occurred if a change in the subj memory results from the read_op Effectively a flow has occurred from the obj to the subj Write External Making a request for the subj to read the obj specified The mod field is ignored and we define that some state change has occurred if a change in the obj memory results from the write op Effectively a flow has occurred from the subj to the obj Table 3 Transaction types supported in model type Input at Flow attran ATTransaction op transition Input System StateMonad Boolean def transition inp sys let policy sys pol in let at inp at in let inputtran inp attran in case inputtran of MakeKnown gt curr currently accessible at if curr amp amp access secure policy srm policy bbm at then add access at return true else return false Terminate gt curr currently accessible at if curr then remove access at return true else return false ReadResourceExt gt curr currently accessible at 74 if curr then b4resourceMem lt get resource memory at subj read op at subj at obj afte
137. the subjects and also the set of system resources RSet System resources are included under State as the memory attribute ResourceMemory of Resource may change with state transition Figure 81 shows the definition of System and State types type System blocks BSet systemflows MM pol Policy sysstate State State contains the flows that are currently enabled for subjects 5 and also the set of system resources type State atset Set Flow resrcset RSet Figure 81 Definition of System and State Figure 82 shows the relationship of the primary model elements of the system Flow is a central model component and is used in State in the definition of the accesses that are enabled in Transform to represent data flow that have been actualized and in the Policy object to define allowed data flows 68 1 NL NN atset Set Flow et Block resrcset RSet 1 1 srm SRMatrix bbm BBMatrix Sas Set BBRecord 1 1 Set Flow n n Block Flow BBRecord Subj Subjec BT Block obj ResourceExt b2 Block fset FlowModeSet fset FlowModeSel 1 1 1 1 1 i Resoucot C ea rosis Resource rscid Resourceld rscid Resourceld rscid Resourceld blkid Blockld blkid Blockld blkid Blockld rscmem ResourceMemory rscmem ResourceMemory rscmem ResourceMemory 1 n n exported active ModeOfFiow Figure 82 System Components and their Relationships c
138. the resource The memory attribute will be used in the formulation of the flow property pertaining to read and write operations 62 type Resourceld String Identifier for block type BlockId Resource type Resource rscid Resourceld blkid BlockId rscmem ResourceMemory Figure 75 Declaration of a Resource A Block is defined to be just strictly a set of Resources without adding an explicit BlockID as an attribute This is to conform to the mathematical notion of a block in a partition facilitates comparison and allows set operations between a Block and the Resource set As a result of this definition a number of helper operations have to be defined to retrieve a Block based on its Blockld and also to retrieve the BlockId from a given Block The operations getBlock and getBlockld used in performing these respective functionalities are implemented as below in Figure 76 Given the set of exported resources ReSet and the partition of those resources P the function RB retrieves the block id from a specified ResourceExt object Note that these operations could have just been left as abstract functions but the team furnished their implementations to make the model as complete as possible In the specification the team was however hampered by the non availability of documentation for the newly released Set Base Library and the lack of helper functions for this Library to iterate and extract Set elements for manipu
139. transited to will be secure based on the defined transition operation Theorem stating change of state is secure theorem transition state secure is fa S State input Input securestate S gt securestate transition input S 2 Figure 67 Theorem Transition State Secure It should not be difficult then to conclude that given an initial empty state which is secure by the theorem EmptySecure the system state will always be secure as a direct result from transition_state_secure i Proving in Isabelle During the session at Kestrel the specification was translated to the Isabelle language and Kestrel provided examples of how to use the Isabelle theorem prover The proof steps are performed using the Isabelle graphical interface as described above which can later by copied into the Specware specification itself to facilitate re proof From this experience we learned that interactive theorem proving is an intense effort that requires detailed knowledge of both the target specification s logic and the proof system our BLP model and the Isabelle theorem prover in this case One example to establish that the dominates operation is a linear ordering was not completed due to time limitations of the visit but illustrated how different specification styles as well as proof strategies can effect the elegance of the proof 3 Discussion and Lessons Learned Many of the lessons learned in the building of this subm
140. turn type is Option Variable which mean that it will return the tuple if it is found if not None will be returned Figure 40 shows the op find variable definition 5 Find the variable from the variable list 5 based on variable name and return the variable op find variable Name MemoryState Option Variable def find variable var name mem state find fn i compare var name i 1 Equal mem state 1 proof Isa simp end proof Figure 40 op find variable definition 38 The update variable definition updates the variable according to the parameter passed in to the definition Figure 41 shows the op update_variable definition Update the varibale with the new value op update variable Name Value Label MemoryState gt MemoryState def update_variable var_name var_value var_Label mem_state let new_var insert var_name var_value var_Label filter fn i gt compare var name i 1 Equal mem state 1 in new var mem state 2 mem state 3 proof Isa simp end proof Figure 41 op update variable definition c Support Functions for Statement Execution StatementSpec sw All the support functions for statement execution are located in StatemaentSpec sw These include read low func read high func assignl func assign2 func and get var value They are used by the FileSystemSpec sw The read low func function calls the read low from MemorySpec sw to read a va
141. uate n 1 proof Isa simp end proof Figure 7 Sample Specware specification 16 consts transition State lt Rightarrow gt State defs transition_def simp transition s lt equiv gt Suc fst s Suc snd s theorem evaluate_Obligation_subtype lt lbrakk gt lt not gt n 0 lt rbrakk gt lt Longrightarrow gt int n 1 lt ge gt 0 by auto fun evaluate nat lt Rightarrow gt State where evaluate 0 1 0 evaluate Suc n transition evaluate n Figure 8 Isabelle specification translated from the sample Specware Specification 3 Basic Specware Operation We can invoke the XEmacs with Specware and Isabelle by running the Specwarelsabelle executable file located in the opt Kertrel Specware 4 2 2 directory Figure 9 shows a screenshot of the XEmacs interface where all the commands can be found in the menu tabs Table 1 lists some of the more common XEmacs and Specware keyboard commands that were used in the development of this thesis The documentation on using Specware can be found in Specware 4 2 User Manual 21 Help Process Current File Process Unit Cc Cp FileSystemSpec sw miss ss Specware eik Generate Lisp Cc g e null x amp amp hd x Yellow 4 Generate amp Load Lisp 9 Aviom ta etata tha stata chances in tha traffic Figure 9 Screenshot of XEmacs for Specware and Isabelle 17 Commands Purpose CTRL x
142. urr fset 71 op add_access at Flow StateMonad curr lt get access by at at if single curr then remove_access at curr at get current access put current access curr at subj at subj obj at obj fset theMember curr fset at fset return else return op remove_access at Flow StateMonad fn S State gt 0 atset S atset fn i gt i subj at subj amp amp i obj at obj resrcset S resrcset op get current access StateMonad Set Flow fn S State gt S atset S op put current access inatset Set Flow StateMonad fn S State gt atset inatset resrcset S resrcset op read op Subject ResourceExt StateMonad op write op Subject ResourceExt StateMonad op get resource StateMonad RSet fn S State gt S resrcset S op get resource memory Resource gt StateMonad Set Bit Figure 86 State Monads for state access and modification e Security Predicates To evaluate the security of the state and its transitions security predicates as shown in Figure 87 are defined to check the security of accesses and the security properties of the system access allowed checks to see if a subject can access an 42 external resource with the mode specified based on system policy access_secure encapsulates the access_allowed providing a check on whethe
143. web Monads are successfully used in the LPSK to model flows between subjects and objects G LPSK The team successfully modeled the notions of state changes and data flows in the LPSK model Compared to Decloss s model the model is more concrete and this is possible with the use of Set notation and Monads The notion of flow is central to the model and is used to represent requests made the access table and also the actualized data flows between resources The system is modeled such that all accesses to systems are arbitrated requests made in the form of transactions The system maintains an access table and grants accesses based on the defined system policy Transactions are divided into two groups those that change the access table and those that change the memory of the resources With the above defined the team formulated security theorems regarding transactions and actualized flows Readers should note that operations are not restricted to the two representative ones ReadResourceExt and WriteResoruceExt currently handled by our model The notion of a secure state is coined based on the existing system state at a point in time A Transaction would result in state changes and hence it is necessary to ensure that a transaction always brings a secure state to another secure state This is ensured if the flow associated with the Transaction is allowed and enabled by the system Conversely the team also successfully depicted in the mod
144. y p evaluate n Figure 11 Example of sub goals in Isabelle before induction is applied proof prove step 1 qoal 2 subgoals 1 property p evaluate 0 2 in property p evaluate n gt property p evaluate Suc n Figure 12 Example of induct tac being applied to the variable n c apply simp add x1 x2 This command will apply a simplification proof strategy by adding x1 and x2 which are theory names as rules for it simplification 2 Structured Isar Proofs Isar stands for Intelligiable semi automated reasoning and is an extension of the apply style proofs 24 Figure 13 shows a typical proof skeleton of Isar proofs and Figure 14 shows an example of Isar proofs in Isabelle More comprehensive coverage on Isar can be found in the Isabelle Isar reference manual 24 19 proof assume he assm have intermediate result have intermediate result show the concl qed Figure 13 Typical proof of skeleton of Isar proofs proof have new state snd MonadBLPSimpleExampleExceptions transition a MakeKnown S insert a S by rule tac MonadBLPSimpleExampleExceptions transition MakeKnown secure from al have S secure S lt subseteq gt MonadBLPSimpleExampleExceptions access secure p by auto simp add MonadBLPSimpleExampleExceptions securestate p def with new state a2 b MakeKnown MonadBLPSimpleExampleExceptions access secure p a show thesis by auto sim
145. ystem by the controlled stepwise introduction of implementation design decisions in such a way that the refined specifications and ultimately the working code is a provably correct refinement of the original problem specification 14 There are three major objectives in the design of Specware First it seeks to provide a way to express requirements as formal specifications independent of the ultimate implementation or target language Users can then focus on correctness which is crucial to the reliability of the system Second it keeps the problem analysis process separated from the implementation process Implementation choices can be introduced piecewise making backtracking and alternative exploration possible Third it allows the articulation of software requirements making of implementation choices and generation of provably correct code in a formally verifiable manner facilitating system maintenance and adaption of specifications to new or changed requirements Specware interfaces with and performs logical inference and proving using external theorem provers like SRI s SNARK theorem prover and Isabelle External provers are connected to Specware through logic morphisms which relate logic to each other SNARK is an automatic theorem prover that is difficult for allowing users to verify the proof as it provides insufficient logging capabilities 2 Isabelle is an interactive theorem prover that provides more feedbacks to the us

complete thesis as PDF

Contents

Download Pdf Manuals

Related Search

Related Contents