Automatic Covert Channel Analysis of a Multilevel Secure Component

  • Ruggero Lanotte
  • Andrea Maggiolo-Schettini
  • Simone Tini
  • Angelo Troina
  • Enrico Tronci
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3269)


The NRL Pump protocol defines a multilevel secure component whose goal is to minimize leaks of information from high level systems to lower level systems, without degrading average time performances. We define a probabilistic model for the NRL Pump and show how a probabilistic model checker (FHP-murϕ) can be used to estimate the capacity of a probabilistic covert channel in the NRL Pump. We are able to compute the probability of a security violation as a function of time for various configurations of the system parameters (e.g. buffer sizes, moving average size, etc). Because of the model complexity, our results cannot be obtained using an analytical approach and, because of the low probabilities involved, it can be hard to obtain them using a simulator.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abbott, R.K., Garcia-Molina, H.: Scheduling Real-Time Transactions: a Performance Evaluation. ACM Trans. Database Syst. 17(3), 513–560 (1992)CrossRefGoogle Scholar
  2. 2.
    Bell, D., La Padula, L.J.: Secure Computer Systems: Unified Exposition and Multics Interpretation. Tech. Rep. ESD-TR-75-301, MITRE MTR-2997 (1976)Google Scholar
  3. 3.
    David, R., Son, S.H.: A Secure Two Phase Locking Protocol. In: Proc. IEEE Symp. on Reliable Distributed Systems, pp. 126–135 (1993)Google Scholar
  4. 4.
    Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite Horizon Analysis of Markov Chains with the Murphi Verifier. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 394–409. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite Horizon Analysis of Stochastic Systems with the Murphi Verifier. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol. 2841, pp. 58–71. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol Verification as a Hardware Design Aid. In: Proc. IEEE Int. Conf. on Computer Design on VLSI in Computer & Processors, pp. 522–525 (1992)Google Scholar
  7. 7.
    Gray, J., Reuter, A.: Transaction Processing: Concepts and Techniques. Morgan Kaufmann Publishers Inc., San Francisco (1992)Google Scholar
  8. 8.
    Kang, M.H., Froscher, J., Moskowitz, I.S.: A Framework for MLS Interoperability. In: Proc. IEEE High Assurance Systems Engineering Workshop, pp. 198–205 (1996)Google Scholar
  9. 9.
    Kang, M.H., Froscher, J., Moskowitz, I.S.: An Architecture for Multilevel Security Interoperability. In: Proc. IEEE Computer Security Application Conf. (1997)Google Scholar
  10. 10.
    Kang, M.H., Moore, A.P., Moskowitz, I.S.: Design and Assurance Strategy for the NRL Pump. IEEE Computer 31(4), 56–64 (1998)Google Scholar
  11. 11.
    Kang, M.H., Moskowitz, I.S.: A Pump for Rapid, Reliable, Secure Communication. In: Proc. ACM Conf. on Computer and Communication Security, pp. 119–129 (1993)Google Scholar
  12. 12.
    Kang, M.H., Moskowitz, I.S., Lee, D.: A Network Pump. IEEE Trans. Software Eng. 22(5), 329–338 (1996)CrossRefGoogle Scholar
  13. 13.
    Moskowitz, I.S., Miller, A.R.: The Channel Capacity of a Certain Noisy Timing Channel. IEEE Trans. Information Theory 38(4) (1992)Google Scholar
  14. 14.
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  16. 16.
    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 52. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Meadows, C.: What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 10–21. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols using Murϕ. In: Proc. IEEE Symp. on Security and Privacy, pp. 141–151 (1997)Google Scholar
  19. 19.
    Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-State Analysis of SSL 3.0. In: Proc. USENIX Security Symp. (1998)Google Scholar
  20. 20.
    Son, S.H., Mukkamala, R., David, R.: Integrating Security and Real-Time Requirements Using Covert Channel Capacity. IEEE Trans. Knowl. Data Eng. 12(6), 865–879 (2000)CrossRefGoogle Scholar
  21. 21.
  22. 22.

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Ruggero Lanotte
    • 1
  • Andrea Maggiolo-Schettini
    • 2
  • Simone Tini
    • 1
  • Angelo Troina
    • 2
  • Enrico Tronci
    • 3
  1. 1.Dipartimento di Scienze della Cultura, Politiche e dell’InformazioneUniversità dell’Insubria 
  2. 2.Dipartimento di InformaticaUniversità di Pisa 
  3. 3.Dipartimento di InformaticaUniversità di Roma “La Sapienza” 

Personalised recommendations