Applications of Logic in Computer Security：逻辑在计算机安全中的应用.ppt

ApplicationsofLogicinComputerSecurityJonathanMillenSRIInternational

AreasofApplicationMultilevelOperatingSystemSecurity“OrangeBook,”CommercialTrustedProductEvaluation,A1-levelEmphasisonsecrecy,security/clearancelevelsAccessControlPoliciesDiscretionaryorrole-basedpoliciesEmphasisonapplication-specificpolicies,integrityPublic-KeyInfrastructureandTrustManagementNetworkanddistributedsystemsecurityDigitallysignedcertificatesforidentityandprivilegesCryptographicAuthenticationProtocolsFornetworkcommunicationconfidentialityandauthenticationOtherareas:databases,firewalls/routers,intrusiondetectionComputerSecurityNetworkSecurity

ContributionsofLogicUndecidabilityResultsSafetyproblemfordiscretionaryaccesscontrolCryptographicprotocolanalysisTheoremProvingEnvironmentsVerifyingcorrectnessofformalOSspecificationsInductiveproofsofcryptographicprotocolsLogicProgrammingPrologprogramsforcryptographicprotocolanalysis,trustmanagementModelCheckingForcryptographicprotocolanalysisSpecializedLogicsForcryptographicprotocolanalysis,trustmanagement

MultilevelOperatingSystemSecurityMotivatedbyprotectionofclassifiedinformationinsharedsystemsHigh-assurance(A1)systemsmayprotectSecretdatafromunclearedusersArchitecture:trustedOSkernel,hardwaresupportAbstractsystemmodelofaccesscontrol:Bell-LaPadula(ca.1975)Structuredstate-transitionsystem:subject-objectaccessmatrix,levelsSecurityinvariantsandtransitionrules(forOSfunctions)“FormalTop-LevelSpecification”(FTLS)Moredetailedstate-transitionsystemFormalProofs:ModeltransitionssatisfyinvariantsFTLSisaninterpretationofthesystemmodelCarriedoutinenvironmentslikeGypsy,FDM,HDMSomeFTLSerrorsreflectedincodewerediscoveredOfHistoricalInterest

AccessControlPoliciesSafetyProblemSubject-object-rightsmatrix“rights”werearbitrary,representingdifferentkindsofaccessOperations:create/dele