Loading...
Please wait, while we are loading the content...
Similar Documents
Cheko: aspect-oriented runtime monitor certification via model-checking (2011).
| Content Provider | CiteSeerX |
|---|---|
| Author | Hamlen, Kevin W. Jones, Micah M. Sridhar, Meera |
| Abstract | In-lining runtime monitors into untrusted binary programs via aspectweaving is an increasingly popular technique for efficiently and flexibly securing untrusted mobile code. However, the complexity of the monitor implementation and in-lining process in these frameworks can lead to vulnerabilities and low assurance for code-consumers. This paper presents a machine-verification technique for aspect-oriented in-lined reference monitors based on abstract interpretation and model-checking. Rather than relying upon trusted advice, the system verifies semantic properties expressed in a purely declarative policy specification language. Experiments on a variety of real-world policies and Java applications demonstrate that the approach is practical and effective. 1 |
| File Format | |
| Publisher Date | 2011-01-01 |
| Access Restriction | Open |
| Subject Keyword | Aspect-oriented Runtime Monitor Certification Real-world Policy Aspect-oriented In-lined Reference Monitor Machine-verification Technique Popular Technique Untrusted Mobile Code Java Application Untrusted Binary Program Monitor Implementation Low Assurance Semantic Property In-lining Runtime Monitor In-lining Process Declarative Policy Specification Language |
| Content Type | Text |
| Resource Type | Article |
