++++++++++++++++++ FME2001: - Review reports for paper 52 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 52 CATEGORY: 2 TITLE: Information Flow Control and Applications - Bridging A Gap - AUTHOR(S): Heiko Mantel -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper is concerned with characterising intransitive information flow properties in nondeterministic systems. Some results (verification conditions) are given which give ways of proving that system descriptions meet such properties. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2.5 Please comment your rating: This work is mostly theoretical, but it is significant and in an area (security) of growing interest to the formal methods community. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 5 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The characterisation of intransitive information flow properties is both new and significant. 6. How WORTHWILE is the goal of the authors? Comment: The goal is extremely worthwhile - this is an importnt problem. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes, they are sound. I did not work through all the proofs completely, but they appear to be sound. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work is theoretical. Some motivation for applicability is given, but this work is not yet at the application stage. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is clear, though the material is rather dense. The paper would benefit from some pictures of traces in illustrating the definitions. The discussion of related work is very good. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Definition 1: I intersect O = {} presumably ? Page 5, views are sometimes presented in the order (V,N,C) (e.g. definition 4) and sometimes in the order (V,C,N) (e.g. in fig 2). Make these consistent to avoid confusion. Almost all of the examples in the paper have N = {}. You do remark on page 7 that the definiiton (of BSD_V) becomes much simpler if N = {}. How much simpler would the results be in cases where N = {} ? Do you get significant simplification in this case? Examples at the end of section 2 would be helpful: one of a system that meets one of your properties, and one of a system that does not. The description of intransitive information flow could be improved. In the first paragraph of section 3, you should say why all defns of information flow are incompatible with intransitive information flow. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 52 CATEGORY: 2 TITLE: Information Flow Control and Applications - Bridging A Gap - AUTHOR(S): Heiko Mantel -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Security models can be described in terms of restrictions on information flow. A way of specifying such restrictions is presented which covers more situations than previously, esp by not insisting on transitivity of restrictions. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2-3 Please comment your rating: Seems a good paper on this topic for an audience whose concerns are more wide spread. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 2 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Removing restricting to transitive policies. 6. How WORTHWILE is the goal of the authors? Comment: Very. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: As far as I can see, they are indeed. From about section 3.4 onward I was not entirely able to follow the arguments. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: Arguments in favor seem to be strong. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Well written. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: End of section 2.1: maybe mention that SES are more expressive than the purely trace based ES. Views are defined as (V,N,C) but seem to be listed as (V,C,N) e.g. in Figure 2. It is not always clear whether "observation" (a term not defined in the paper) refers to "trace" or "event" - seems to be the latter? I am not convinced that the simplifications "as in [Man00b]" (page 14) do not restrict expressiveness. If they don't, they might be stated as a normalisation theorem earlier on. Page 17: I don't know what it means for a semantics to be "in general superior" to another. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 52 CATEGORY: 2 TITLE: Information Flow Control and Applications - Bridging A Gap - AUTHOR(S): Heiko Mantel -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The author extends his previous proposal for a generic security model [Man00a] in order to cope with intransitive flow policies in non-deterministic systems. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: This paper does not fit exactly in the theme "F.M. for increasing software productivity" but rather the classical "F.M. for increasing software quality". 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 5 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Several generalizations of "non-interference" for non-deterministic systems have been proposed but they fail to express "intransitive flow policies". The presented model seems to capture such flows policies (unfortunately, no formal proof is possible for this step, so the author gives such evidence based on examples) 6. How WORTHWILE is the goal of the authors? Comment: Once accepted that intransitive flow policies are important for "real life" applications (the author give examples and point several references) then it is certainly desirable to capture such policies in non-deterministic models. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Good. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: A section is devoted to the derivation of an "unwinding theorem" that give a concrete methodology for proving that a given system satisfy a certain flow policy (given that it satisfy certain conditions). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Is good. 11. Were there any formatting or mechanical problems with this paper?: No. Are the figures and length acceptable?: Yes. Are the references correct?: Yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++