Types for Information Flow Control: Labeling Granularity and Semantic Models