Parametric information flow control in ehealth

We study the problem of enforcing information flow control (IFC) in ehealth systems to verify secure flow of information through programs. IFC mechanisms allow users to control the release and propagation of sensitive information so that confidential information is not observable to unintended principals while collaborating with other legitimate principals. We formalise the parametrised security classes that are required for security policy specification in typical e-health systems in a hospital and use static type checking for detecting security policy violations in the system. The key advantage of using the parametrised security class lattice is greater precision in stating policies, enhanced usability and a reduced overhead in creating security tags.