| Presentation | 2000/9/22 A Security Verification Method for Programs with Stack Inspection Satoshi Ikada, Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Java development kit 1.2 provides a runtime access control mechanism which inspects the control stack to check that the program has appropriate access permission. For such a programming language, it is desirable to guarantee that each execution of a program satisfies required security properties. Jensen et al. introduced a verification problem of deciding for a given program P and a given security property F written in a temporal logic formula, whether every reachable state of P satisfies F. They showed that the problem is decidable for the class of programs which do not contain mutual recursion. In this paper, it is shown that the set of state sequences (traces) of a program is always an indexed language and consequently the verification problem is decidable. Our result is stronger than Jensen's in that a security property can be specified as a regular language, whose expressive power is properly stronger than temporal logic, and a program can contain mutual recursion. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | access control / security verification / indexed language / stack inspection / Java |
| Paper # | ISEC2000-78 |
| Date of Issue |
| Conference Information | |
| Committee | ISEC |
|---|---|
| Conference Date | 2000/9/22(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Information Security (ISEC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Security Verification Method for Programs with Stack Inspection |
| Sub Title (in English) | |
| Keyword(1) | access control |
| Keyword(2) | security verification |
| Keyword(3) | indexed language |
| Keyword(4) | stack inspection |
| Keyword(5) | Java |
| 1st Author's Name | Satoshi Ikada |
| 1st Author's Affiliation | Graduate School of Information Science, Nara Institute of Science and Technology() |
| 2nd Author's Name | Naoya Nitta |
| 2nd Author's Affiliation | Graduate School of Information Science, Nara Institute of Science and Technology |
| 3rd Author's Name | Yoshiaki Takata |
| 3rd Author's Affiliation | Graduate School of Information Science, Nara Institute of Science and Technology |
| 4th Author's Name | Hiroyuki Seki |
| 4th Author's Affiliation | Graduate School of Information Science, Nara Institute of Science and Technology |
| Date | 2000/9/22 |
| Paper # | ISEC2000-78 |
| Volume (vol) | vol.100 |
| Number (no) | 324 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |