Bucketing is a technique proposed to mitigate timing channel attacks by restricting a system’s outputs to only occur at designated time intervals. Bucketing has the effect of reducing the possible timing channel observations to a small number of possibilities. In this paper, we present an approach to formally prove the security of systems under the bucketing technique. First, we show that bucketing alone is insufficient to ensure security against adversaries who can make multiple side channel observations. Then, we present a condition sufficient to guarantee a system’s security against adaptive side-channel-observing adversaries. Roughly, the condition says that there exists a large enough subset of secrets on which the system’s side channel reveals no more information than that revealed by its regular channel and that the regular channel is secure to a certain degree on the subset. We also present a condition which guarantees that the system would satisfy the first condition when bucketing is applied. This second condition says that the system’s side-channel outputs are independent of attacker-controlled inputs (but can depend on secrets) and that the regular channel is secure to a certain degree. We show that the two conditions facilitate proving security of systems under adaptive side-channel attacks by separating the concerns of regular-channel security from side-channel information leakage. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of them are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.