发明名称 |
采用逻辑消解的安全语言转换 |
摘要 |
安全语言构造可被转换成逻辑语言构造,反之亦然。逻辑消解可例如使用逻辑语言构造来实现。在一示例实现中,描述了将安全语言断言转换成至少一个逻辑语言规则。在另一示例实现中,描述了将反映一逻辑语言的证明图转换成反映一安全语言的证明图。在又一示例实现中,描述了使用确定性算法对逻辑语言程序的求值。 |
申请公布号 |
CN101512505B |
申请公布日期 |
2011.09.07 |
申请号 |
CN200780033329.6 |
申请日期 |
2007.09.10 |
申请人 |
微软公司 |
发明人 |
B·B·迪拉韦;C·富尔内;A·D·戈登;M·Y·贝克;J·F·麦凯 |
分类号 |
G06F15/00(2006.01)I |
主分类号 |
G06F15/00(2006.01)I |
代理机构 |
上海专利商标事务所有限公司 31100 |
代理人 |
顾嘉运 |
主权项 |
一种从安全语言到逻辑语言的转换方法,所述逻辑语言是受约束的Datalog,所述方法包括:对包括所断言的事实以及零或多个条件事实的安全语言断言,确定所断言的事实是否是平面的,所述安全语言的断言格式为:如果一个或多个其它事实有效且满足某组条件,则安全主体陈述一事实有效;如果所断言的事实被确定为是平面的,则将所述安全语言断言转换成包括对应于所断言的事实的主要事实以及对应于所述零或多个条件事实的零个或多个副条件的逻辑语言规则,当且仅当没有出现‘能够断言’,所断言的事实是平面的;如果所断言的事实未被确定为是平面的,则通过以下步骤将所述安全语言断言转换成逻辑语言规则:添加包括对应于所断言的事实的主要事实以及对应于所述零或多个条件事实的零或多个副条件的逻辑语言规则;以及对所断言的事实的每一委托指示动词,添加具有无界委托深度以及表示被委托方的新变量的逻辑语言规则;对断言上下文中的每一安全语言断言重复所述确定和转换,以产生逻辑语言程序;以及结合授权查询对所述逻辑语言程序求值,以产生指示应许可还是拒绝对某一资源的访问的授权输出。 |
地址 |
美国华盛顿州 |